theorem th (h : 2 = 2) : 2 = 2

theorem th2 : 2 = 2

theorem plus_comm (a b : ℕ) : a + b = b + a

theorem alg (a b c : ℕ) : a * (b + c) = a * (c + b)

theorem alg' (a b c d : ℕ) : (c + d) ^ 2 + c * (a + b) ^ 2 = c ^ 2 + d ^ 2 + 2 * c * d + c * a ^ 2 + c * (b ^ 2 + 2 * a * b)

theorem ev10 : Even 10

theorem two_div_even (n : ℕ) : Even n → 2 ∣ n

theorem two_div_ten : 2 ∣ 10

def PrimeNum (n : ℕ) : Prop

Equations

• PrimeNum n = (n ≥ 2 ∧ ∀ (m : ℕ), m ∣ n → m = 1 ∨ m = n)

theorem notprime_1 : ¬PrimeNum 1

theorem notprime_9 : ¬PrimeNum 9

theorem prime_5 : PrimeNum 5

theorem irrat_pow_irrat_rat : ∃ (x : ℝ) (y : ℝ), Irrational x ∧ Irrational y ∧ ¬Irrational (x ^ y)

theorem infinites_prime (n : ℕ) : ∃ (p : ℕ), Nat.Prime p ∧ p > n

theorem example_3 (n : ℕ) (hn : n ≥ 4) : n ^ 3 < 3 ^ n

theorem example_4 (n : ℕ) (hn : n ≥ 4) : n.factorial > 2 ^ n

def TriangleNumber.triangular_number (n : ℕ) : ℕ

Equations

• TriangleNumber.triangular_number n = ∑ k ∈ Finset.range (n + 1), k

theorem TriangleNumber.closed_form_triangular (n : ℕ) : triangular_number n = n * (n + 1) / 2

theorem TriangleNumber.odd_squared_minus_one_dvd_eight (n : ℕ) (h_odd : Odd n) : 8 ∣ n ^ 2 - 1

theorem TrigButEulerFunny.cos_x_from_exp_ix (x : ℂ) : Complex.cos x = (Complex.exp (x * Complex.I) + Complex.exp (-x * Complex.I)) / 2

theorem TrigButEulerFunny.sin_x_from_exp_ix (x : ℂ) : Complex.sin x = (Complex.exp (x * Complex.I) - Complex.exp (-x * Complex.I)) / (2 * Complex.I)

theorem TrigButEulerFunny.sin_sq_add_cos_sq (x : ℂ) : Complex.sin x ^ 2 + Complex.cos x ^ 2 = 1

theorem TrigButEulerFunny.sin_two_x (x : ℂ) : Complex.sin (2 * x) = 2 * Complex.sin x * Complex.cos x