Loogle!

Result

Found 348 declarations mentioning Nat.choose. Of these, only the first 200 are shown.

• Nat.choose 📋 Mathlib.Data.Nat.Choose.Basic
  : ℕ → ℕ → ℕ
• Nat.choose_eq_fast_choose 📋 Mathlib.Data.Nat.Choose.Basic
  : Nat.choose = Nat.fast_choose
• Nat.choose_mono 📋 Mathlib.Data.Nat.Choose.Basic
  (b : ℕ) : Monotone fun a => a.choose b
• Nat.choose_one_right 📋 Mathlib.Data.Nat.Choose.Basic
  (n : ℕ) : n.choose 1 = n
• Nat.choose_self 📋 Mathlib.Data.Nat.Choose.Basic
  (n : ℕ) : n.choose n = 1
• Nat.choose_le_succ 📋 Mathlib.Data.Nat.Choose.Basic
  (a c : ℕ) : a.choose c ≤ a.succ.choose c
• Nat.choose_succ_self 📋 Mathlib.Data.Nat.Choose.Basic
  (n : ℕ) : n.choose n.succ = 0
• Nat.choose_zero_right 📋 Mathlib.Data.Nat.Choose.Basic
  (n : ℕ) : n.choose 0 = 1
• Nat.choose_zero_succ 📋 Mathlib.Data.Nat.Choose.Basic
  (k : ℕ) : Nat.choose 0 k.succ = 0
• Nat.choose_eq_zero_of_lt 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} : n < k → n.choose k = 0
• Nat.choose_le_choose 📋 Mathlib.Data.Nat.Choose.Basic
  {a b : ℕ} (c : ℕ) (h : a ≤ b) : a.choose c ≤ b.choose c
• Nat.choose_ne_zero 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} (h : k ≤ n) : n.choose k ≠ 0
• Nat.choose_eq_zero_iff 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} : n.choose k = 0 ↔ n < k
• Nat.choose_ne_zero_iff 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} : n.choose k ≠ 0 ↔ k ≤ n
• Nat.choose_pos 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} : k ≤ n → 0 < n.choose k
• Nat.choose_eq_descFactorial_div_factorial 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.choose k = n.descFactorial k / k.factorial
• Nat.descFactorial_eq_factorial_mul_choose 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.descFactorial k = k.factorial * n.choose k
• Nat.choose_le_add 📋 Mathlib.Data.Nat.Choose.Basic
  (a b c : ℕ) : a.choose c ≤ (a + b).choose c
• Nat.choose_le_middle 📋 Mathlib.Data.Nat.Choose.Basic
  (r n : ℕ) : n.choose r ≤ n.choose (n / 2)
• Nat.choose_succ_succ 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.succ.choose k.succ = n.choose k + n.choose k.succ
• Nat.choose_symm 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} (hk : k ≤ n) : n.choose (n - k) = n.choose k
• Nat.choose_symm_of_eq_add 📋 Mathlib.Data.Nat.Choose.Basic
  {n a b : ℕ} (h : n = a + b) : n.choose a = n.choose b
• Nat.choose_eq_one_iff 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} : n.choose k = 1 ↔ k = 0 ∨ n = k
• Nat.choose_symm_add 📋 Mathlib.Data.Nat.Choose.Basic
  {a b : ℕ} : (a + b).choose a = (a + b).choose b
• Nat.multichoose_eq 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.multichoose k = (n + k - 1).choose k
• Nat.choose_succ_self_right 📋 Mathlib.Data.Nat.Choose.Basic
  (n : ℕ) : (n + 1).choose n = n + 1
• Nat.ascFactorial_eq_factorial_mul_choose 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : (n + 1).ascFactorial k = k.factorial * (n + k).choose k
• Nat.ascFactorial_eq_factorial_mul_choose' 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.ascFactorial k = k.factorial * (n + k - 1).choose k
• Nat.choose_eq_asc_factorial_div_factorial 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : (n + k).choose k = (n + 1).ascFactorial k / k.factorial
• Nat.choose_eq_asc_factorial_div_factorial' 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : (n + k - 1).choose k = n.ascFactorial k / k.factorial
• Nat.choose_eq_factorial_div_factorial 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} (hk : k ≤ n) : n.choose k = n.factorial / (k.factorial * (n - k).factorial)
• Nat.choose_le_succ_of_lt_half_left 📋 Mathlib.Data.Nat.Choose.Basic
  {r n : ℕ} (h : r < n / 2) : n.choose r ≤ n.choose (r + 1)
• Nat.choose_mul_factorial_mul_factorial 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} : k ≤ n → n.choose k * k.factorial * (n - k).factorial = n.factorial
• Nat.add_choose 📋 Mathlib.Data.Nat.Choose.Basic
  (i j : ℕ) : (i + j).choose j = (i + j).factorial / (i.factorial * j.factorial)
• Nat.add_choose_mul_factorial_mul_factorial 📋 Mathlib.Data.Nat.Choose.Basic
  (i j : ℕ) : (i + j).choose j * i.factorial * j.factorial = (i + j).factorial
• Nat.choose_two_right 📋 Mathlib.Data.Nat.Choose.Basic
  (n : ℕ) : n.choose 2 = n * (n - 1) / 2
• Nat.choose_mul 📋 Mathlib.Data.Nat.Choose.Basic
  {n k s : ℕ} (hsk : s ≤ k) : n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
• Nat.choose_succ_left 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) (hk : 0 < k) : (n + 1).choose k = n.choose (k - 1) + n.choose k
• Nat.choose_succ_succ' 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : (n + 1).choose (k + 1) = n.choose k + n.choose (k + 1)
• Nat.choose_succ_right_eq 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
• Nat.choose_mul_right 📋 Mathlib.Data.Nat.Choose.Basic
  {m n : ℕ} (hn : n ≠ 0) : (m * n).choose n = m * (m * n - 1).choose (n - 1)
• Nat.choose_symm_half 📋 Mathlib.Data.Nat.Choose.Basic
  (m : ℕ) : (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m
• Nat.choose_mul_succ_eq 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
• Nat.add_one_mul_choose_eq 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : (n + 1) * n.choose k = (n + 1).choose (k + 1) * (k + 1)
• Nat.choose_eq_choose_pred_add 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} (hn : 0 < n) (hk : 0 < k) : n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k
• Nat.choose_succ_right 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) (hn : 0 < n) : n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)
• Nat.choose_mul_add 📋 Mathlib.Data.Nat.Choose.Basic
  {m n : ℕ} (hn : n ≠ 0) : (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)
• Finset.card_product_filter_lt 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {s : Finset α} [LinearOrder α] : {x ∈ s ×ˢ s | x.1 < x.2}.card = s.card.choose 2
• Fintype.card_product_filter_lt 📋 Mathlib.Data.Fintype.Prod
  {α : Type u_1} [Fintype α] [LinearOrder α] : {x | x.1 < x.2}.card = (Fintype.card α).choose 2
• List.length_sublistsLen 📋 Mathlib.Data.List.Sublists
  {α : Type u} (n : ℕ) (l : List α) : (List.sublistsLen n l).length = l.length.choose n
• Multiset.card_powersetCard 📋 Mathlib.Data.Multiset.Powerset
  {α : Type u_1} (n : ℕ) (s : Multiset α) : (Multiset.powersetCard n s).card = s.card.choose n
• Finset.card_powersetCard 📋 Mathlib.Data.Finset.Powerset
  {α : Type u_1} (n : ℕ) (s : Finset α) : (Finset.powersetCard n s).card = s.card.choose n
• Finset.card_filter_powersetCard_subset 📋 Mathlib.Data.Finset.Powerset
  {α : Type u_1} [DecidableEq α] (s t : Finset α) (n : ℕ) (hst : s ⊆ t) (hsn : s.card ≤ n) : {x ∈ Finset.powersetCard n t | s ⊆ x}.card = (t.card - s.card).choose (n - s.card)
• Fintype.card_finset_len 📋 Mathlib.Data.Fintype.Powerset
  {α : Type u_1} [Fintype α] (k : ℕ) : Fintype.card { s // s.card = k } = (Fintype.card α).choose k
• Set.ncard_powerset_ncard 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s : Set α} (hs : s.Finite) (n : ℕ) : {t | t ⊆ s ∧ t.ncard = n}.ncard = s.ncard.choose n
• Nat.sum_range_multichoose 📋 Mathlib.Data.Nat.Choose.Sum
  (n k : ℕ) : ∑ i ∈ Finset.range (n + 1), k.multichoose i = (n + k).choose k
• Nat.sum_range_choose 📋 Mathlib.Data.Nat.Choose.Sum
  (n : ℕ) : ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n
• Nat.sum_Icc_choose 📋 Mathlib.Data.Nat.Choose.Sum
  (n k : ℕ) : ∑ m ∈ Finset.Icc k n, m.choose k = (n + 1).choose (k + 1)
• Nat.choose_middle_le_pow 📋 Mathlib.Data.Nat.Choose.Sum
  (n : ℕ) : (2 * n + 1).choose n ≤ 4 ^ n
• Finset.sum_powerset_apply_card 📋 Mathlib.Data.Nat.Choose.Sum
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] (f : ℕ → α) {x : Finset β} : ∑ m ∈ x.powerset, f m.card = ∑ m ∈ Finset.range (x.card + 1), x.card.choose m • f m
• Finset.sum_antidiagonal_choose_add 📋 Mathlib.Data.Nat.Choose.Sum
  (d n : ℕ) : ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
• Nat.sum_range_choose_halfway 📋 Mathlib.Data.Nat.Choose.Sum
  (m : ℕ) : ∑ i ∈ Finset.range (m + 1), (2 * m + 1).choose i = 4 ^ m
• Int.alternating_sum_range_choose_of_ne 📋 Mathlib.Data.Nat.Choose.Sum
  {n : ℕ} (h0 : n ≠ 0) : ∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = 0
• Nat.four_pow_le_two_mul_add_one_mul_central_binom 📋 Mathlib.Data.Nat.Choose.Sum
  (n : ℕ) : 4 ^ n ≤ (2 * n + 1) * (2 * n).choose n
• Nat.sum_range_add_choose 📋 Mathlib.Data.Nat.Choose.Sum
  (n k : ℕ) : ∑ i ∈ Finset.range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)
• Nat.sum_range_mul_choose 📋 Mathlib.Data.Nat.Choose.Sum
  (n : ℕ) : ∑ i ∈ Finset.range (n + 1), i * n.choose i = n * 2 ^ (n - 1)
• Int.alternating_sum_range_choose 📋 Mathlib.Data.Nat.Choose.Sum
  {n : ℕ} : ∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0
• Int.alternating_sum_range_choose_eq_choose 📋 Mathlib.Data.Nat.Choose.Sum
  {n m : ℕ} : ∑ k ∈ Finset.range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)
• Commute.add_pow' 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [Semiring R] {x y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
• Commute.add_pow 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [Semiring R] {x y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
• add_pow 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
• Finset.prod_antidiagonal_pow_choose_succ 📋 Mathlib.Data.Nat.Choose.Sum
  {M : Type u_2} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 = (∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) * ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2
• Finset.sum_antidiagonal_choose_succ_nsmul 📋 Mathlib.Data.Nat.Choose.Sum
  {M : Type u_2} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), (n + 1).choose ij.1 • f ij.1 ij.2 = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 • f ij.1 (ij.2 + 1) + ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.2 • f (ij.1 + 1) ij.2
• Finset.prod_pow_choose_succ 📋 Mathlib.Data.Nat.Choose.Sum
  {M : Type u_2} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∏ i ∈ Finset.range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i = (∏ i ∈ Finset.range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ Finset.range (n + 1), f (i + 1) (n - i) ^ n.choose i
• Finset.sum_choose_succ_nsmul 📋 Mathlib.Data.Nat.Choose.Sum
  {M : Type u_2} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∑ i ∈ Finset.range (n + 2), (n + 1).choose i • f i (n + 1 - i) = ∑ i ∈ Finset.range (n + 1), n.choose i • f i (n + 1 - i) + ∑ i ∈ Finset.range (n + 1), n.choose i • f (i + 1) (n - i)
• Finset.sum_antidiagonal_choose_succ_mul 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) + ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
• sub_pow 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [CommRing R] (x y : R) (n : ℕ) : (x - y) ^ n = ∑ m ∈ Finset.range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
• Finset.sum_choose_succ_mul 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : ∑ i ∈ Finset.range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)
• Polynomial.coeff_X_add_one_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  (R : Type u_1) [Semiring R] (n k : ℕ) : ((Polynomial.X + 1) ^ n).coeff k = ↑(n.choose k)
• Polynomial.coeff_one_add_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  (R : Type u_1) [Semiring R] (n k : ℕ) : ((1 + Polynomial.X) ^ n).coeff k = ↑(n.choose k)
• Polynomial.coeff_X_add_C_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (r : R) (n k : ℕ) : ((Polynomial.X + Polynomial.C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)
• Polynomial.one_add_X_pow_sub_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {S : Type u_1} [CommRing S] (d : ℕ) : (1 + Polynomial.X) ^ d - Polynomial.X ^ d = ∑ i ∈ Finset.range d, d.choose i • Polynomial.X ^ i
• Polynomial.eval_monomial_one_add_sub 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {S : Type v} [CommRing S] (d : ℕ) (y : S) : Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) = ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
• Polynomial.geom_sum_X_comp_X_add_one_eq_sum 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (∑ i ∈ Finset.range n, Polynomial.X ^ i).comp (Polynomial.X + 1) = ∑ i ∈ Finset.range n, ↑(n.choose (i + 1)) * Polynomial.X ^ i
• Nat.choose_le_descFactorial 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) : n.choose k ≤ n.descFactorial k
• Nat.choose_le_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) : n.choose k ≤ n ^ k
• Nat.choose_lt_descFactorial 📋 Mathlib.Data.Nat.Choose.Bounds
  {n k : ℕ} (hk : 2 ≤ k) (hkn : k ≤ n) : n.choose k < n.descFactorial k
• Nat.choose_le_two_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) : n.choose k ≤ 2 ^ n
• Nat.choose_lt_two_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) (p : 0 < n) : n.choose k < 2 ^ n
• Nat.choose_succ_le_two_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) : (n + 1).choose k ≤ 2 ^ n
• Nat.choose_lt_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  {n k : ℕ} (hn : n ≠ 0) (hk : 2 ≤ k) : n.choose k < n ^ k
• Nat.choose_add_le_add_one_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) : (n + k).choose k ≤ (n + 1) ^ k
• Nat.choose_le_sub_pow 📋 Mathlib.Data.Nat.Choose.Bounds
  (n k : ℕ) : n.choose k ≤ (n + 1 - k) ^ k
• Nat.choose_le_pow_div 📋 Mathlib.Data.Nat.Choose.Bounds
  {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (r n : ℕ) : ↑(n.choose r) ≤ ↑n ^ r / ↑r.factorial
• Nat.choose_lt_pow_div 📋 Mathlib.Data.Nat.Choose.Bounds
  {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {n k : ℕ} (hn : n ≠ 0) (hk : 2 ≤ k) : ↑(n.choose k) < ↑n ^ k / ↑k.factorial
• Nat.pow_le_choose 📋 Mathlib.Data.Nat.Choose.Bounds
  {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (r n : ℕ) : ↑(n + 1 - r) ^ r / ↑r.factorial ≤ ↑(n.choose r)
• Nat.centralBinom_eq_two_mul_choose 📋 Mathlib.Data.Nat.Choose.Central
  (n : ℕ) : n.centralBinom = (2 * n).choose n
• Nat.choose_le_centralBinom 📋 Mathlib.Data.Nat.Choose.Central
  (r n : ℕ) : (2 * n).choose r ≤ n.centralBinom
• List.sum_fixedLengthDigits_sum 📋 Mathlib.Data.Nat.Digits.Lemmas
  {b : ℕ} (hb : 1 < b) (l : ℕ) : ∑ L ∈ List.fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
• Nat.sum_sum_digits_eq 📋 Mathlib.Data.Nat.Digits.Lemmas
  {b : ℕ} (hb : 1 < b) (l : ℕ) : ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2
• Nat.factorization_choose_le_log 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} : (n.choose k).factorization p ≤ Nat.log p n
• Nat.factorization_choose_eq_zero_of_lt 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (h : n < p) : (n.choose k).factorization p = 0
• Nat.pow_factorization_choose_le 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (hn : 0 < n) : p ^ (n.choose k).factorization p ≤ n
• Nat.factorization_choose_le_one 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (p_large : n < p ^ 2) : (n.choose k).factorization p ≤ 1
• Nat.prod_pow_factorization_choose 📋 Mathlib.Data.Nat.Choose.Factorization
  (n k : ℕ) (hkn : k ≤ n) : ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k
• Nat.factorization_choose_of_lt_three_mul 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (hp' : p ≠ 2) (hk : p ≤ k) (hk' : p ≤ n - k) (hn : n < 3 * p) : (n.choose k).factorization p = 0
• Nat.factorization_le_factorization_choose_add 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} : k ≤ n → k ≠ 0 → n.factorization p ≤ (n.choose k).factorization p + k.factorization p
• Nat.factorization_choose_prime_pow 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (hp : Nat.Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : ((p ^ n).choose k).factorization p = n - k.factorization p
• Nat.factorization_choose_prime_pow_add_factorization 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (hp : Nat.Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : ((p ^ n).choose k).factorization p + k.factorization p = n
• Nat.factorization_choose' 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k b : ℕ} (hp : Nat.Prime p) (hnb : Nat.log p (n + k) < b) : ((n + k).choose k).factorization p = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card
• Nat.factorization_choose 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k b : ℕ} (hp : Nat.Prime p) (hkn : k ≤ n) (hnb : Nat.log p n < b) : (n.choose k).factorization p = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
• Nat.Prime.emultiplicity_le_emultiplicity_choose_add 📋 Mathlib.Data.Nat.Multiplicity
  {p : ℕ} (hp : Nat.Prime p) (n k : ℕ) : emultiplicity p n ≤ emultiplicity p (n.choose k) + emultiplicity p k
• Nat.Prime.dvd_choose_pow 📋 Mathlib.Data.Nat.Multiplicity
  {p n k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣ (p ^ n).choose k
• Nat.Prime.dvd_choose_pow_iff 📋 Mathlib.Data.Nat.Multiplicity
  {p n k : ℕ} (hp : Nat.Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n
• Nat.Prime.emultiplicity_choose_prime_pow 📋 Mathlib.Data.Nat.Multiplicity
  {p n k : ℕ} (hp : Nat.Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)
• Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity 📋 Mathlib.Data.Nat.Multiplicity
  {p n k : ℕ} (hp : Nat.Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : emultiplicity p ((p ^ n).choose k) + emultiplicity p k = ↑n
• Nat.Prime.emultiplicity_choose' 📋 Mathlib.Data.Nat.Multiplicity
  {p n k b : ℕ} (hp : Nat.Prime p) (hnb : Nat.log p (n + k) < b) : emultiplicity p ((n + k).choose k) = ↑{i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card
• Nat.Prime.emultiplicity_choose 📋 Mathlib.Data.Nat.Multiplicity
  {p n k b : ℕ} (hp : Nat.Prime p) (hkn : k ≤ n) (hnb : Nat.log p n < b) : emultiplicity p (n.choose k) = ↑{i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
• Commute.add_pow_prime_eq' 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x y : R} (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
• add_pow_prime_eq' 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x y : R) : (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
• Commute.add_pow_prime_eq 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x y : R} (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Finset.Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
• add_pow_prime_eq 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x y : R) : (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Finset.Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
• Commute.add_pow_prime_pow_eq' 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
• add_pow_prime_pow_eq' 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x y : R) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
• Commute.add_pow_prime_pow_eq 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * x * y * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)
• add_pow_prime_pow_eq 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x y : R) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * x * y * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)
• Polynomial.iterate_derivative_eq_factorial_smul_sum 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] p = k.factorial • ∑ x ∈ ((⇑Polynomial.derivative)^[k] p).support, Polynomial.C ((x + k).choose k • p.coeff (x + k)) * Polynomial.X ^ x
• Polynomial.iterate_derivative_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) : (⇑Polynomial.derivative)^[n] (p * q) = ∑ k ∈ Finset.range n.succ, n.choose k • ((⇑Polynomial.derivative)^[n - k] p * (⇑Polynomial.derivative)^[k] q)
• Polynomial.iterate_derivative_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (n m : ℕ) (p : Polynomial R) : (⇑Polynomial.derivative)^[n] (p * Polynomial.X ^ m) = ∑ k ∈ Finset.range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑Polynomial.derivative)^[n - k] p * Polynomial.X ^ (m - k))
• Finset.prod_powersetCard 📋 Mathlib.Algebra.BigOperators.Group.Finset.Powerset
  {α : Type u_1} {β : Type u_2} [CommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) : ∏ t ∈ Finset.powersetCard n s, f t.card = f n ^ s.card.choose n
• Finset.sum_powersetCard 📋 Mathlib.Algebra.BigOperators.Group.Finset.Powerset
  {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) : ∑ t ∈ Finset.powersetCard n s, f t.card = s.card.choose n • f n
• List.length_sym2 📋 Mathlib.Data.List.Sym
  {α : Type u_1} {xs : List α} : xs.sym2.length = (xs.length + 1).choose 2
• Multiset.card_sym2 📋 Mathlib.Data.Multiset.Sym
  {α : Type u_1} {m : Multiset α} : m.sym2.card = (m.card + 1).choose 2
• Finset.card_sym2 📋 Mathlib.Data.Finset.Sym
  {α : Type u_1} (s : Finset α) : s.sym2.card = (s.card + 1).choose 2
• Nat.cast_choose 📋 Mathlib.Data.Nat.Choose.Cast
  (K : Type u_1) [DivisionSemiring K] [CharZero K] {a b : ℕ} (h : a ≤ b) : ↑(b.choose a) = ↑b.factorial / (↑a.factorial * ↑(b - a).factorial)
• Nat.cast_add_choose 📋 Mathlib.Data.Nat.Choose.Cast
  (K : Type u_1) [DivisionSemiring K] [CharZero K] {a b : ℕ} : ↑((a + b).choose a) = ↑(a + b).factorial / (↑a.factorial * ↑b.factorial)
• Nat.cast_choose_two 📋 Mathlib.Data.Nat.Choose.Cast
  (K : Type u_1) [DivisionRing K] [NeZero 2] (a : ℕ) : ↑(a.choose 2) = ↑a * (↑a - 1) / 2
• Nat.add_choose_eq 📋 Mathlib.Data.Nat.Choose.Vandermonde
  (m n k : ℕ) : (m + n).choose k = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k, m.choose ij.1 * n.choose ij.2
• Nat.sum_range_choose_sq 📋 Mathlib.Data.Nat.Choose.Vandermonde
  (n : ℕ) : ∑ i ∈ Finset.range (n + 1), n.choose i ^ 2 = (2 * n).choose n
• Polynomial.hasseDeriv_coeff 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) (n : ℕ) : ((Polynomial.hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)
• Polynomial.hasseDeriv_apply 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) : (Polynomial.hasseDeriv k) f = f.sum fun i r => (Polynomial.monomial (i - k)) (↑(i.choose k) * r)
• Polynomial.hasseDeriv_monomial 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (k n : ℕ) (r : R) : (Polynomial.hasseDeriv k) ((Polynomial.monomial n) r) = (Polynomial.monomial (n - k)) (↑(n.choose k) * r)
• Polynomial.hasseDeriv_comp 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (k l : ℕ) : Polynomial.hasseDeriv k ∘ₗ Polynomial.hasseDeriv l = (k + l).choose k • Polynomial.hasseDeriv (k + l)
• Set.powersetCard.card 📋 Mathlib.Data.Set.PowersetCard
  (α : Type u_1) (n : ℕ) : Nat.card ↑(Set.powersetCard α n) = (Nat.card α).choose n
• Nat.fib_succ_eq_sum_choose 📋 Mathlib.Data.Nat.Fib.Basic
  (n : ℕ) : Nat.fib (n + 1) = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, p.1.choose p.2
• fwdDiff_choose 📋 Mathlib.Algebra.Group.ForwardDiff
  {R : Type u_3} [CommRing R] (j : ℕ) : (fwdDiff 1 fun x => ↑(x.choose (j + 1))) = fun x => ↑(x.choose j)
• fwdDiff_iter_choose 📋 Mathlib.Algebra.Group.ForwardDiff
  {R : Type u_3} [CommRing R] (j k : ℕ) : ((fwdDiff 1)^[k] fun x => ↑(x.choose (k + j))) = fun x => ↑(x.choose j)
• fwdDiff_iter_choose_zero 📋 Mathlib.Algebra.Group.ForwardDiff
  {R : Type u_3} [CommRing R] (m n : ℕ) : (fwdDiff 1)^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0
• shift_eq_sum_fwdDiff_iter 📋 Mathlib.Algebra.Group.ForwardDiff
  {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (n : ℕ) (y : M) : f (y + n • h) = ∑ k ∈ Finset.range (n + 1), n.choose k • (fwdDiff h)^[k] f y
• sum_range_shift_eq_sum_fwdDiff_iter 📋 Mathlib.Algebra.Group.ForwardDiff
  {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (y : M) (n : ℕ) : ∑ k ∈ Finset.range n, f (y + k • h) = ∑ k ∈ Finset.range n, n.choose (k + 1) • (fwdDiff h)^[k] f y
• fwdDiff_iter_eq_sum_shift 📋 Mathlib.Algebra.Group.ForwardDiff
  {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (f : M → G) (n : ℕ) (y : M) : (fwdDiff h)^[n] f y = ∑ k ∈ Finset.range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)
• LieModule.toEnd_pow_lie 📋 Mathlib.Algebra.Lie.OfAssociative
  (R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x y : L) (z : M) (n : ℕ) : ((LieModule.toEnd R L M) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieModule.toEnd R L M) x ^ ij.2) z⁆
• LieAlgebra.ad_pow_lie 📋 Mathlib.Algebra.Lie.OfAssociative
  (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x y z : L) (n : ℕ) : ((LieAlgebra.ad R L) x ^ n) ⁅y, z⁆ = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieAlgebra.ad R L) x ^ ij.2) z⁆
• LieDerivation.iterate_apply_lie 📋 Mathlib.Algebra.Lie.Derivation.Basic
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (a b : L) : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
• LieDerivation.iterate_apply_lie' 📋 Mathlib.Algebra.Lie.Derivation.Basic
  {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (a b : L) : (⇑D)^[n] ⁅a, b⁆ = ∑ i ∈ Finset.range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆
• Nat.cast_choose_eq_descPochhammer_div 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (K : Type u_1) [DivisionRing K] [CharZero K] (a b : ℕ) : ↑(a.choose b) = Polynomial.eval (↑a) (descPochhammer K b) / ↑b.factorial
• Nat.cast_choose_eq_ascPochhammer_div 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (K : Type u_1) [DivisionSemiring K] [CharZero K] (a b : ℕ) : ↑(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b.factorial
• exteriorPower.finrank_eq 📋 Mathlib.LinearAlgebra.ExteriorPower.Basis
  (R : Type u_1) (M : Type u_3) (n : ℕ) [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [Nontrivial R] : Module.finrank R ↥(⋀[R]^n M) = (Module.finrank R M).choose n
• Nat.stirlingFirst_succ_self_left 📋 Mathlib.Combinatorics.Enumerative.Stirling
  (n : ℕ) : (n + 1).stirlingFirst n = (n + 1).choose 2
• Nat.stirlingSecond_succ_self_left 📋 Mathlib.Combinatorics.Enumerative.Stirling
  (n : ℕ) : (n + 1).stirlingSecond n = (n + 1).choose 2
• summable_choose_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable fun n => ↑((n + k).choose k) * r ^ n
• hasSum_choose_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
• tsum_choose_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = Ring.inverse (1 - r) ^ (k + 1)
• hasSum_choose_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun n => ↑((n + k).choose k) * r ^ n) (1 / (1 - r) ^ (k + 1))
• tsum_choose_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = 1 / (1 - r) ^ (k + 1)
• Multiset.multinomial_cons 📋 Mathlib.Data.Nat.Choose.Multinomial
  (x : ℕ) (m : Multiset ℕ) : (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial
• List.multinomial_cons 📋 Mathlib.Data.Nat.Choose.Multinomial
  (x : ℕ) (l : List ℕ) : (x :: l).multinomial = (x + l.sum).choose x * l.multinomial
• Nat.binomial_eq_choose 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} {f : α → ℕ} {a b : α} [DecidableEq α] (h : a ≠ b) : Nat.multinomial {a, b} f = (f a + f b).choose (f a)
• Multiset.countPerms_filter_ne 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} [DecidableEq α] (a : α) (m : Multiset α) : m.countPerms = m.card.choose (Multiset.count a m) * (Multiset.filter (fun x => a ≠ x) m).countPerms
• Nat.multinomial_cons 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (f : α → ℕ) : Nat.multinomial (Finset.cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * Nat.multinomial s f
• Multiset.multinomial_add 📋 Mathlib.Data.Nat.Choose.Multinomial
  (m m' : Multiset ℕ) : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
• Finsupp.multinomial_update 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} (a : α) (f : α →₀ ℕ) : f.multinomial = (f.sum fun x => id).choose (f a) * (f.update a 0).multinomial
• Nat.multinomial_insert 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) : Nat.multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * Nat.multinomial s f
• Sym.countPerms_coe_fill_of_notMem 📋 Mathlib.Data.Nat.Choose.Multinomial
  {n : ℕ} {α : Type u_1} [DecidableEq α] {m : Fin (n + 1)} {s : Sym α (n - ↑m)} {x : α} (hx : x ∉ s) : (↑(Sym.fill x m s)).countPerms = n.choose ↑m * (↑s).countPerms
• MvPolynomial.coeff_add_pow 📋 Mathlib.Algebra.MvPolynomial.Coeff
  {R : Type u_1} [CommSemiring R] (d : Fin 2 →₀ ℕ) (n : ℕ) : MvPolynomial.coeff d ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n) = ↑(if (d 0, d 1) ∈ Finset.HasAntidiagonal.antidiagonal n then n.choose (d 0) else 0)
• Sym2.card 📋 Mathlib.Data.Sym.Card
  {α : Type u_2} [Fintype α] : Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2
• Sym.card_sym_eq_choose 📋 Mathlib.Data.Sym.Card
  {α : Type u_2} [Fintype α] (k : ℕ) [Fintype (Sym α k)] : Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose k
• Sym2.card_image_offDiag 📋 Mathlib.Data.Sym.Card
  {α : Type u_1} [DecidableEq α] (s : Finset α) : (Finset.image (Function.uncurry Sym2.mk) s.offDiag).card = s.card.choose 2
• Sym2.card_subtype_not_diag 📋 Mathlib.Data.Sym.Card
  {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2
• Sym2.card_diagSet_compl 📋 Mathlib.Data.Sym.Card
  {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype.card ↑Sym2.diagSetᶜ = (Fintype.card α).choose 2
• Finset.card_finsuppAntidiag_nat_eq_choose 📋 Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
  {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (n : ℕ) : (s.finsuppAntidiag n).card = (s.card + n - 1).choose n
• PowerSeries.coeff_subst_X_zero_add_X_one 📋 Mathlib.RingTheory.PowerSeries.Substitution
  {R : Type u_2} [CommRing R] (f : PowerSeries R) (e : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff e) (PowerSeries.subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) = ↑((e 0 + e 1).choose (e 0)) * (PowerSeries.coeff (e 0 + e 1)) f
• iteratedDeriv_fun_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (fun i => f i * g i) x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x
• iteratedDeriv_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (f * g) x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x
• iteratedDerivWithin_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f * g) s x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDerivWithin i f s x * iteratedDerivWithin (n - i) g s x
• iteratedDerivWithin_smul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Module 𝔸 F] [IsBoundedSMul 𝔸 F] [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f • g) s x = ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
• Polynomial.coeff_le_of_roots_le 📋 Mathlib.Topology.Algebra.Polynomial
  {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {p : Polynomial F} {f : F →+* K} {B : ℝ} (i : ℕ) (h1 : p.Monic) (h2 : (Polynomial.map f p).Splits) (h3 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) : ‖(Polynomial.map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)
• Polynomial.coeff_bdd_of_roots_le 📋 Mathlib.Topology.Algebra.Polynomial
  {F : Type u_3} {K : Type u_4} [CommRing F] [NormedField K] {B : ℝ} {d : ℕ} (f : F →+* K) {p : Polynomial F} (h1 : p.Monic) (h2 : (Polynomial.map f p).Splits) (h3 : p.natDegree ≤ d) (h4 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B) (i : ℕ) : ‖(Polynomial.map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
• NumberField.Embeddings.coeff_bdd_of_norm_le 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  {K : Type u_1} [Field K] [NumberField K] {A : Type u_2} [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {B : ℝ} {x : K} (h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B) (i : ℕ) : ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ Module.finrank ℚ K * ↑((Module.finrank ℚ K).choose (Module.finrank ℚ K / 2))
• sub_one_mul_padicValNat_choose_eq_sub_sum_digits 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p k n : ℕ} [hp : Fact (Nat.Prime p)] (h : k ≤ n) : (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum
• sub_one_mul_padicValNat_choose_eq_sub_sum_digits' 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p k n : ℕ} [hp : Fact (Nat.Prime p)] : (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
• padicValNat_choose' 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p n k b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p (n + k) < b) : padicValNat p ((n + k).choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card
• padicValNat_choose 📋 Mathlib.NumberTheory.Padics.PadicVal.Basic
  {p n k b : ℕ} [hp : Fact (Nat.Prime p)] (hkn : k ≤ n) (hnb : Nat.log p n < b) : padicValNat p (n.choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
• Ring.choose_natCast 📋 Mathlib.RingTheory.Binomial
  {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (n k : ℕ) : Ring.choose (↑n) k = ↑(n.choose k)
• Ring.choose_smul_choose 📋 Mathlib.RingTheory.Binomial
  {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) {n k : ℕ} (hkn : k ≤ n) : n.choose k • Ring.choose r n = Ring.choose r k * Ring.choose (r - ↑k) (n - k)
• Ring.choose_add_smul_choose 📋 Mathlib.RingTheory.Binomial
  {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) (n k : ℕ) : (n + k).choose k • Ring.choose (r + ↑k) (n + k) = Ring.choose (r + ↑k) k * Ring.choose r n
• Ring.descPochhammer_smeval_add 📋 Mathlib.RingTheory.Binomial
  {R : Type u_1} [Ring R] {r s : R} (k : ℕ) (h : Commute r s) : (descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
• Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero 📋 Mathlib.Analysis.Analytic.Binomial
  (a : ℕ) : HasFPowerSeriesOnBall (fun x => 1 / (1 - x) ^ (a + 1)) (FormalMultilinearSeries.ofScalars ℂ fun n => ↑((a + n).choose a)) 0 1
• Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero 📋 Mathlib.Analysis.Analytic.Binomial
  (a : ℕ) {r : ℝ} (hr : r ≠ 0) : HasFPowerSeriesOnBall (fun x => 1 / (r - x) ^ (a + 1)) (FormalMultilinearSeries.ofScalars ℝ fun n => (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖r‖ₑ
• Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero 📋 Mathlib.Analysis.Analytic.Binomial
  (a : ℕ) {z : ℂ} (hz : z ≠ 0) : HasFPowerSeriesOnBall (fun x => 1 / (z - x) ^ (a + 1)) (FormalMultilinearSeries.ofScalars ℂ fun n => (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59