theoremvandermonde (m n r : ℕ) : Nat.choose (m + n) r = ∑ k ∈ Finset.range (r + 1), Nat.choose m k * Nat.choose n (r - k) := by rw [Nat.add_choose_eq] rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
theoremgeom_sum_finite {R : Type*} [CommRing R] (x : R) (n : ℕ) (h : x ≠ 1) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1 := by have _ := h exact geom_sum_mul x n
theoremcrt {m n : ℕ} (h : Nat.Coprime m n) (a b : ℤ) : ∃ x : ℤ, x ≡ a [ZMOD m] ∧ x ≡ b [ZMOD n] := by by_cases hm : m = 0 · subst hm have hn : n = 1 := by rwa [Nat.Coprime, Nat...
theoremincl_excl_two {α : Type*} [DecidableEq α] (A B : Finset α) : (A ∪ B).card = A.card + B.card - (A ∩ B).card := by have := Finset.card_union_add_card_inter A B omega
theorembinomial_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