51.

closed binomial_thm

Binomial theorem

theorem binomial_thm {R : Type*} [CommSemiring R] (x y : R) (n : ℕ) : (x + y) ^ n = ∑ k ∈ Finset.range (n + 1), Nat.choose n k * x ^ k * y ^ (n - k) := by rw [add_pow] congr 1 ext k ring

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

52.

closed euler_thm

Euler's theorem (modular)

theorem euler_thm (n : ℕ) (a : ℤ) (h : IsCoprime a n) : a ^ Nat.totient n ≡ 1 [ZMOD n] := by by_cases hn : n = 0 · subst hn simp haveI : NeZero n := ⟨hn⟩ rw [← ZMod.in...

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

53.

closed fermat_little

Fermat's little theorem

theorem fermat_little (p : ℕ) (hp : p.Prime) (a : ℤ) (h : ¬ (p : ℤ) ∣ a) : a ^ (p - 1) ≡ 1 [ZMOD p] := by have hpn : IsCoprime a (p : ℤ) := by rw [Int.isCoprime_iff_nat_coprime] si...

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

54.

closed wilson

Wilson's theorem

theorem wilson (p : ℕ) (hp : p.Prime) : (Nat.factorial (p - 1)) % p = p - 1 := by have h_neg : (-1 : ZMod p).val = p - 1 := by have h_p : p = (p - 1) + 1 :=...

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

55.

closed bezout

Bezout's identity

theorem bezout (a b : ℤ) (h : a ≠ 0 ∨ b ≠ 0) : ∃ x y : ℤ, a * x + b * y = Int.gcd a b := by have _ := h use Int.gcdA a b, Int.gcdB a b exact (Int.gcd_eq_gcd_ab a b).symm

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

56.

closed triangle_ineq

Triangle inequality (real)

theorem triangle_ineq (a b : ℝ) : |a + b| ≤ |a| + |b| := abs_add_le a b

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

57.

closed cauchy_schwarz_real

Schwarz inequality (real)

theorem cauchy_schwarz_real {n : ℕ} (x y : Fin n → ℝ) : (∑ i, x i * y i) ^ 2 ≤ (∑ i, x i ^ 2) * (∑ i, y i ^ 2) := Finset.sum_mul_sq_le_sq_mul_sq Finset.univ x y

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

58.

closed bool_and_comm

Boolean and is commutative

theorem bool_and_comm (a b : Bool) : (a && b) = (b && a) := by cases a <;> cases b <;> rfl

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

59.

closed option_map_some

Option map of some

theorem option_map_some {α β : Type} (f : α → β) (a : α) : (Option.some a).map f = Option.some (f a) := rfl

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →

60.

closed list_length_map

List map preserves length

theorem list_length_map {α β : Type} (f : α → β) (l : List α) : (l.map f).length = l.length := List.length_map f

posted about 1 month ago · proven 20 days ago

Rewards

no reward

View proof →