Loogle!

Result

Found 435 declarations mentioning Nat.factorial. Of these, only the first 200 are shown.

• Nat.factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  : ℕ → ℕ
• Nat.factorial_eq_factorialBinarySplitting 📋 Mathlib.Data.Nat.Factorial.Basic
  : Nat.factorial = Nat.factorialBinarySplitting
• Nat.self_le_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : n ≤ n.factorial
• Nat.descFactorial_self 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : n.descFactorial n = n.factorial
• Nat.factorial_ne_zero 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : n.factorial ≠ 0
• Nat.factorial_pos 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : 0 < n.factorial
• Nat.one_ascFactorial 📋 Mathlib.Data.Nat.Factorial.Basic
  (k : ℕ) : Nat.ascFactorial 1 k = k.factorial
• Nat.factorial_one 📋 Mathlib.Data.Nat.Factorial.Basic
  : Nat.factorial 1 = 1
• Nat.factorial_two 📋 Mathlib.Data.Nat.Factorial.Basic
  : Nat.factorial 2 = 2
• Nat.factorial_zero 📋 Mathlib.Data.Nat.Factorial.Basic
  : Nat.factorial 0 = 1
• Nat.factorial_dvd_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} (h : m ≤ n) : m.factorial ∣ n.factorial
• Nat.factorial_le 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} (h : m ≤ n) : m.factorial ≤ n.factorial
• Nat.lt_factorial_self 📋 Mathlib.Data.Nat.Factorial.Basic
  {n : ℕ} (hi : 3 ≤ n) : n < n.factorial
• Nat.factorial_le_pow 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : n.factorial ≤ n ^ n
• Nat.factorial_eq_one 📋 Mathlib.Data.Nat.Factorial.Basic
  {n : ℕ} : n.factorial = 1 ↔ n ≤ 1
• Nat.one_lt_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {n : ℕ} : 1 < n.factorial ↔ 1 < n
• Nat.dvd_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} : 0 < m → m ≤ n → m ∣ n.factorial
• Nat.factorial_inj 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} (hn : 1 < n) : n.factorial = m.factorial ↔ n = m
• Nat.factorial_lt_of_lt 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} (hn : 0 < n) (h : n < m) : n.factorial < m.factorial
• Nat.factorial_lt 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} (hn : 0 < n) : n.factorial < m.factorial ↔ n < m
• Nat.ascFactorial_le_factorial_mul_pow 📋 Mathlib.Data.Nat.Factorial.Basic
  (n k : ℕ) : n.ascFactorial k ≤ k.factorial * n ^ k
• Nat.descFactorial_eq_div 📋 Mathlib.Data.Nat.Factorial.Basic
  {n k : ℕ} (h : k ≤ n) : n.descFactorial k = n.factorial / (n - k).factorial
• Nat.factorial_mul_descFactorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {n k : ℕ} : k ≤ n → (n - k).factorial * n.descFactorial k = n.factorial
• Nat.factorial_inj' 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} (h : 1 < n ∨ 1 < m) : n.factorial = m.factorial ↔ n = m
• Nat.add_factorial_le_factorial_add 📋 Mathlib.Data.Nat.Factorial.Basic
  (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i + n.factorial ≤ (i + n).factorial
• Nat.mul_factorial_pred 📋 Mathlib.Data.Nat.Factorial.Basic
  {n : ℕ} (hn : n ≠ 0) : n * (n - 1).factorial = n.factorial
• Nat.ascFactorial_eq_div 📋 Mathlib.Data.Nat.Factorial.Basic
  (n k : ℕ) : (n + 1).ascFactorial k = (n + k).factorial / n.factorial
• Nat.factorial_mul_ascFactorial 📋 Mathlib.Data.Nat.Factorial.Basic
  (n k : ℕ) : n.factorial * (n + 1).ascFactorial k = (n + k).factorial
• Nat.factorial_succ 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial
• Nat.factorial_mul_pow_sub_le_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {n m : ℕ} (hnm : n ≤ m) : n.factorial * n ^ (m - n) ≤ m.factorial
• Nat.add_factorial_lt_factorial_add 📋 Mathlib.Data.Nat.Factorial.Basic
  {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) : i + n.factorial < (i + n).factorial
• Nat.two_pow_mul_factorial_le_factorial_two_mul 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : 2 ^ n * n.factorial ≤ (2 * n).factorial
• Nat.factorial_mul_pow_le_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {m n : ℕ} : m.factorial * (m + 1) ^ n ≤ (m + n).factorial
• Nat.add_factorial_succ_le_factorial_add_succ 📋 Mathlib.Data.Nat.Factorial.Basic
  (i n : ℕ) : i + (n + 1).factorial ≤ (i + (n + 1)).factorial
• Nat.factorial_two_mul_le 📋 Mathlib.Data.Nat.Factorial.Basic
  (n : ℕ) : (2 * n).factorial ≤ (2 * n) ^ n * n.factorial
• Nat.add_factorial_succ_lt_factorial_add_succ 📋 Mathlib.Data.Nat.Factorial.Basic
  {i : ℕ} (n : ℕ) (hi : 2 ≤ i) : i + (n + 1).factorial < (i + n + 1).factorial
• Nat.ascFactorial_eq_div' 📋 Mathlib.Data.Nat.Factorial.Basic
  (n k : ℕ) (h : 0 < n) : n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial
• Nat.factorial_mul_ascFactorial' 📋 Mathlib.Data.Nat.Factorial.Basic
  (n k : ℕ) (h : 0 < n) : (n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial
• Nat.factorial_dvd_ascFactorial 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : k.factorial ∣ n.ascFactorial k
• Nat.factorial_dvd_descFactorial 📋 Mathlib.Data.Nat.Choose.Basic
  (n k : ℕ) : k.factorial ∣ n.descFactorial 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.factorial_mul_factorial_dvd_factorial_add 📋 Mathlib.Data.Nat.Choose.Basic
  (i j : ℕ) : i.factorial * j.factorial ∣ (i + j).factorial
• Nat.factorial_mul_factorial_dvd_factorial 📋 Mathlib.Data.Nat.Choose.Basic
  {n k : ℕ} (hk : k ≤ n) : k.factorial * (n - k).factorial ∣ n.factorial
• 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_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
• Finset.prod_Ico_id_eq_factorial 📋 Mathlib.Algebra.BigOperators.Intervals
  (n : ℕ) : ∏ x ∈ Finset.Ico 1 (n + 1), x = n.factorial
• List.length_permutations 📋 Mathlib.Data.List.Permutation
  {α : Type u_1} (l : List α) : l.permutations.length = l.length.factorial
• List.length_permutationsAux 📋 Mathlib.Data.List.Permutation
  {α : Type u_1} (ts is : List α) : (ts.permutationsAux is).length + is.length.factorial = (ts.length + is.length).factorial
• Function.injective_iff_iterate_factorial_card_eq_id 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} [Fintype α] : Function.Injective f ↔ f^[(Fintype.card α).factorial] = id
• Function.isPeriodicPt_factorial_card_of_mem_periodicPts 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} {x : α} [Fintype α] (h : x ∈ Function.periodicPts f) : Function.IsPeriodicPt f (Fintype.card α).factorial x
• Function.mem_periodicPts_iff_isPeriodicPt_factorial_card 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} {x : α} [Fintype α] : x ∈ Function.periodicPts f ↔ Function.IsPeriodicPt f (Fintype.card α).factorial x
• 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.factorization_factorial_eq_zero_of_lt 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n : ℕ} (h : n < p) : n.factorial.factorization p = 0
• Nat.factorization_factorial_le_div_pred 📋 Mathlib.Data.Nat.Choose.Factorization
  {p : ℕ} (hp : Nat.Prime p) (n : ℕ) : n.factorial.factorization p ≤ n / (p - 1)
• Nat.factorization_factorial_mul 📋 Mathlib.Data.Nat.Choose.Factorization
  {n p : ℕ} (hp : Nat.Prime p) : (p * n).factorial.factorization p = n.factorial.factorization p + n
• Nat.sub_one_mul_factorization_factorial 📋 Mathlib.Data.Nat.Choose.Factorization
  {n p : ℕ} (hp : Nat.Prime p) : (p - 1) * n.factorial.factorization p = n - (p.digits n).sum
• Nat.factorization_factorial 📋 Mathlib.Data.Nat.Choose.Factorization
  {p : ℕ} (hp : Nat.Prime p) {n b : ℕ} : Nat.log p n < b → n.factorial.factorization p = ∑ i ∈ Finset.Ico 1 b, n / p ^ i
• Nat.factorization_factorial_mul_succ 📋 Mathlib.Data.Nat.Choose.Factorization
  {n p : ℕ} (hp : Nat.Prime p) : (p * (n + 1)).factorial.factorization p = (p * n).factorial.factorization p + (n + 1).factorization p + 1
• Nat.emultiplicity_two_factorial_lt 📋 Mathlib.Data.Nat.Multiplicity
  {n : ℕ} : n ≠ 0 → emultiplicity 2 n.factorial < ↑n
• Nat.Prime.emultiplicity_factorial_le_div_pred 📋 Mathlib.Data.Nat.Multiplicity
  {p : ℕ} (hp : Nat.Prime p) (n : ℕ) : emultiplicity p n.factorial ≤ ↑(n / (p - 1))
• Nat.Prime.emultiplicity_factorial_mul 📋 Mathlib.Data.Nat.Multiplicity
  {n p : ℕ} (hp : Nat.Prime p) : emultiplicity p (p * n).factorial = emultiplicity p n.factorial + ↑n
• Nat.Prime.multiplicity_factorial_pow 📋 Mathlib.Data.Nat.Multiplicity
  {n p : ℕ} (hp : Nat.Prime p) : multiplicity p (p ^ n).factorial = ∑ i ∈ Finset.range n, p ^ i
• Nat.Prime.sub_one_mul_multiplicity_factorial 📋 Mathlib.Data.Nat.Multiplicity
  {n p : ℕ} (hp : Nat.Prime p) : (p - 1) * multiplicity p n.factorial = n - (p.digits n).sum
• Nat.Prime.emultiplicity_factorial 📋 Mathlib.Data.Nat.Multiplicity
  {p : ℕ} (hp : Nat.Prime p) {n b : ℕ} : Nat.log p n < b → emultiplicity p n.factorial = ↑(∑ i ∈ Finset.Ico 1 b, n / p ^ i)
• Nat.Prime.pow_dvd_factorial_iff 📋 Mathlib.Data.Nat.Multiplicity
  {p n r b : ℕ} (hp : Nat.Prime p) (hbn : Nat.log p n < b) : p ^ r ∣ n.factorial ↔ r ≤ ∑ i ∈ Finset.Ico 1 b, n / p ^ i
• Nat.Prime.emultiplicity_factorial_mul_succ 📋 Mathlib.Data.Nat.Multiplicity
  {n p : ℕ} (hp : Nat.Prime p) : emultiplicity p (p * (n + 1)).factorial = emultiplicity p (p * n).factorial + emultiplicity p (n + 1) + 1
• 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_X_sub_pow_self 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (n : ℕ) (c : R) : (⇑Polynomial.derivative)^[n] ((Polynomial.X - Polynomial.C c) ^ n) = ↑n.factorial
• Polynomial.iterate_derivative_prod_X_sub_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] {k : ℕ} {S : Finset R} (hk : k ≤ S.card) : (⇑Polynomial.derivative)^[k] (∏ a ∈ S, (Polynomial.X - Polynomial.C a)) = ↑k.factorial * ∑ T ∈ Finset.powersetCard (S.card - k) S, ∏ a ∈ T, (Polynomial.X - Polynomial.C a)
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.eval_iterate_derivative_rootMultiplicity 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.eval t ((⇑Polynomial.derivative)^[Polynomial.rootMultiplicity t p] p) = (Polynomial.rootMultiplicity t p).factorial • Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p)
• card_perms_of_finset 📋 Mathlib.Data.Fintype.Perm
  {α : Type u_1} [DecidableEq α] (s : Finset α) : (permsOfFinset s).card = s.card.factorial
• length_permsOfList 📋 Mathlib.Data.Fintype.Perm
  {α : Type u_1} [DecidableEq α] (l : List α) : (permsOfList l).length = l.length.factorial
• Fintype.card_perm 📋 Mathlib.Data.Fintype.Perm
  {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype.card (Equiv.Perm α) = (Fintype.card α).factorial
• Fintype.card_equiv 📋 Mathlib.Data.Fintype.Perm
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] (e : α ≃ β) : Fintype.card (α ≃ β) = (Fintype.card α).factorial
• Nat.card_perm 📋 Mathlib.Data.Finite.Perm
  {α : Type u_1} [Finite α] : Nat.card (Equiv.Perm α) = (Nat.card α).factorial
• AlternatingMap.coe_alternatization 📋 Mathlib.LinearAlgebra.Alternating.Basic
  {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') : MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a
• Nat.eventually_pow_lt_factorial_sub 📋 Mathlib.Order.Filter.AtTopBot.Finite
  (c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c ^ n < (n - d).factorial
• Nat.eventually_mul_pow_lt_factorial_sub 📋 Mathlib.Order.Filter.AtTopBot.Finite
  (a c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < (n - d).factorial
• 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)
• Polynomial.factorial_smul_hasseDeriv 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (k : ℕ) : ⇑(k.factorial • Polynomial.hasseDeriv k) = (⇑Polynomial.derivative)^[k]
• fwdDiff_iter_eq_factorial 📋 Mathlib.Algebra.Group.ForwardDiff
  {R : Type u_3} [CommRing R] {n : ℕ} : ((fwdDiff 1)^[n] fun r => r ^ n) = ↑n.factorial
• Polynomial.fwdDiff_iter_degree_eq_factorial 📋 Mathlib.Algebra.Group.ForwardDiff
  {R : Type u_3} [CommRing R] (P : Polynomial R) : ((fwdDiff 1)^[P.natDegree] fun x => Polynomial.eval x P) = P.leadingCoeff • ↑P.natDegree.factorial
• IsNilpotent.exp_eq_sum 📋 Mathlib.RingTheory.Nilpotent.Exp
  {A : Type u_1} [Ring A] [Module ℚ A] {a : A} {k : ℕ} (h : a ^ k = 0) : IsNilpotent.exp a = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i
• IsNilpotent.exp_smul_eq_sum 📋 Mathlib.RingTheory.Nilpotent.Exp
  {A : Type u_1} [Ring A] [Module ℚ A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module ℚ M] {a : A} {m : M} {k : ℕ} (h : a ^ k • m = 0) (hn : IsNilpotent a) : IsNilpotent.exp a • m = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i • m
• Nat.monotone_factorial 📋 Mathlib.Data.Nat.Factorial.BigOperators
  : Monotone Nat.factorial
• Nat.prod_factorial_pos 📋 Mathlib.Data.Nat.Factorial.BigOperators
  {α : Type u_1} (s : Finset α) (f : α → ℕ) : 0 < ∏ i ∈ s, (f i).factorial
• Finset.prod_range_add_one_eq_factorial 📋 Mathlib.Data.Nat.Factorial.BigOperators
  (n : ℕ) : ∏ i ∈ Finset.range n, (i + 1) = n.factorial
• Nat.factorial_eq_prod_range_add_one 📋 Mathlib.Data.Nat.Factorial.BigOperators
  (n : ℕ) : n.factorial = ∏ i ∈ Finset.range n, (i + 1)
• Nat.prod_factorial_dvd_factorial_sum 📋 Mathlib.Data.Nat.Factorial.BigOperators
  {α : Type u_1} (s : Finset α) (f : α → ℕ) : ∏ i ∈ s, (f i).factorial ∣ (∑ i ∈ s, f i).factorial
• Nat.factorial_coe_dvd_prod 📋 Mathlib.Data.Nat.Factorial.BigOperators
  (k : ℕ) (n : ℤ) : ↑k.factorial ∣ ∏ i ∈ Finset.range k, (n + ↑i)
• Nat.prod_Icc_factorial 📋 Mathlib.Data.Nat.Factorial.SuperFactorial
  (n : ℕ) : ∏ x ∈ Finset.Icc 1 n, x.factorial = n.superFactorial
• Nat.prod_range_factorial_succ 📋 Mathlib.Data.Nat.Factorial.SuperFactorial
  (n : ℕ) : ∏ x ∈ Finset.range n, (x + 1).factorial = n.superFactorial
• Nat.prod_range_succ_factorial 📋 Mathlib.Data.Nat.Factorial.SuperFactorial
  (n : ℕ) : ∏ x ∈ Finset.range (n + 1), x.factorial = n.superFactorial
• Nat.superFactorial_succ 📋 Mathlib.Data.Nat.Factorial.SuperFactorial
  (n : ℕ) : n.succ.superFactorial = (n + 1).factorial * n.superFactorial
• Nat.superFactorial_two_mul 📋 Mathlib.Data.Nat.Factorial.SuperFactorial
  (n : ℕ) : (2 * n).superFactorial = (∏ i ∈ Finset.range n, (2 * i + 1).factorial) ^ 2 * 2 ^ n * n.factorial
• Nat.superFactorial_four_mul 📋 Mathlib.Data.Nat.Factorial.SuperFactorial
  (n : ℕ) : (4 * n).superFactorial = ((∏ i ∈ Finset.range (2 * n), (2 * i + 1).factorial) * 2 ^ n) ^ 2 * (2 * n).factorial
• ascPochhammer_eval_one 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (S : Type u_2) [Semiring S] (n : ℕ) : Polynomial.eval 1 (ascPochhammer S n) = ↑n.factorial
• Nat.cast_factorial 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (S : Type u_1) [Semiring S] (a : ℕ) : ↑a.factorial = Polynomial.eval 1 (ascPochhammer S a)
• 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
• factorial_mul_ascPochhammer 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  (S : Type u_2) [Semiring S] (r n : ℕ) : ↑r.factorial * Polynomial.eval (↑r + 1) (ascPochhammer S n) = ↑(r + n).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
• Lagrange.eval_iterate_derivative_eq_sum 📋 Mathlib.LinearAlgebra.Lagrange
  {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (hvs : Set.InjOn v ↑s) {P : Polynomial F} (hP : P.degree < ↑s.card) {k : ℕ} (hk : k < s.card) (x : F) : Polynomial.eval x ((⇑Polynomial.derivative)^[k] P) = ↑k.factorial * ∑ i ∈ s, (Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a)
• Lagrange.iterate_derivative_interpolate 📋 Mathlib.LinearAlgebra.Lagrange
  {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) {k : ℕ} (hk : k < s.card) : (⇑Polynomial.derivative)^[k] ((Lagrange.interpolate s v) r) = ↑k.factorial * ∑ i ∈ s, Polynomial.C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (Polynomial.X - Polynomial.C (v a))
• factorial_tendsto_atTop 📋 Mathlib.Analysis.SpecificLimits.Basic
  : Filter.Tendsto Nat.factorial Filter.atTop Filter.atTop
• tendsto_factorial_div_pow_self_atTop 📋 Mathlib.Analysis.SpecificLimits.Basic
  : Filter.Tendsto (fun n => ↑n.factorial / ↑n ^ n) Filter.atTop (nhds 0)
• Mathlib.Meta.NormNum.isNat_factorial 📋 Mathlib.Tactic.NormNum.NatFactorial
  {n x : ℕ} (h₁ : Mathlib.Meta.NormNum.IsNat n x) (a : ℕ) (h₂ : Nat.ascFactorial 1 x = a) : Mathlib.Meta.NormNum.IsNat n.factorial a
• Real.pow_div_factorial_le_exp 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℝ) (hx : 0 ≤ x) (n : ℕ) : x ^ n / ↑n.factorial ≤ Real.exp x
• Complex.isCauSeq_exp 📋 Mathlib.Analysis.Complex.Exponential
  (z : ℂ) : IsCauSeq (fun x => ‖x‖) fun n => ∑ m ∈ Finset.range n, z ^ m / ↑m.factorial
• Real.sum_le_exp_of_nonneg 📋 Mathlib.Analysis.Complex.Exponential
  {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial ≤ Real.exp x
• Complex.isCauSeq_norm_exp 📋 Mathlib.Analysis.Complex.Exponential
  (z : ℂ) : IsCauSeq abs fun n => ∑ m ∈ Finset.range n, ‖z ^ m / ↑m.factorial‖
• Real.expNear_sub 📋 Mathlib.Analysis.Complex.Exponential
  (n : ℕ) (x r₁ r₂ : ℝ) : Real.expNear n x r₁ - Real.expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)
• Complex.norm_exp_sub_sum_le_norm_mul_exp 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℂ) (n : ℕ) : ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖
• Real.exp_approx_start 📋 Mathlib.Analysis.Complex.Exponential
  (x a b : ℝ) (h : |Real.exp x - Real.expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b) : |Real.exp x - a| ≤ b
• Complex.norm_exp_sub_sum_le_exp_norm_sub_sum 📋 Mathlib.Analysis.Complex.Exponential
  (x : ℂ) (n : ℕ) : ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ Real.exp ‖x‖ - ∑ m ∈ Finset.range n, ‖x‖ ^ m / ↑m.factorial
• Real.exp_approx_end 📋 Mathlib.Analysis.Complex.Exponential
  (n m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) : |Real.exp x - Real.expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)
• Complex.exp_bound 📋 Mathlib.Analysis.Complex.Exponential
  {x : ℂ} (hx : ‖x‖ ≤ 1) {n : ℕ} (hn : 0 < n) : ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
• Real.exp_bound 📋 Mathlib.Analysis.Complex.Exponential
  {x : ℝ} (hx : |x| ≤ 1) {n : ℕ} (hn : 0 < n) : |Real.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
• Real.exp_bound' 📋 Mathlib.Analysis.Complex.Exponential
  {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) {n : ℕ} (hn : 0 < n) : Real.exp x ≤ ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
• Complex.exp_bound' 📋 Mathlib.Analysis.Complex.Exponential
  {x : ℂ} {n : ℕ} (hx : ‖x‖ / ↑n.succ ≤ 1 / 2) : ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2
• Real.exp_approx_end' 📋 Mathlib.Analysis.Complex.Exponential
  {n : ℕ} {x a b : ℝ} (m : ℕ) (e₁ : n + 1 = m) (rm : ℝ) (er : ↑m = rm) (h : |x| ≤ 1) (e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)) : |Real.exp x - Real.expNear n x a| ≤ |x| ^ n / ↑n.factorial * b
• Complex.sum_div_factorial_le 📋 Mathlib.Analysis.Complex.Exponential
  {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (n j : ℕ) (hn : 0 < n) : ∑ m ∈ Finset.range j with n ≤ m, 1 / ↑m.factorial ≤ ↑n.succ / (↑n.factorial * ↑n)
• Real.exp_1_approx_succ_eq 📋 Mathlib.Analysis.Complex.Exponential
  {n : ℕ} {a₁ b₁ : ℝ} {m : ℕ} (en : n + 1 = m) {rm : ℝ} (er : ↑m = rm) (h : |Real.exp 1 - Real.expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)) : |Real.exp 1 - Real.expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁
• Real.exp_approx_succ 📋 Mathlib.Analysis.Complex.Exponential
  {n : ℕ} {x a₁ b₁ : ℝ} (m : ℕ) (e₁ : n + 1 = m) (a₂ b₂ : ℝ) (e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂) (h : |Real.exp x - Real.expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂) : |Real.exp x - Real.expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
• Nat.stirlingFirst_one_right 📋 Mathlib.Combinatorics.Enumerative.Stirling
  (n : ℕ) : (n + 1).stirlingFirst 1 = n.factorial
• Real.summable_pow_div_factorial 📋 Mathlib.Analysis.SpecificLimits.Normed
  (x : ℝ) : Summable fun n => x ^ n / ↑n.factorial
• hasSum_descFactorial_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (j : ℕ) {r : R} (h : ‖r‖ < 1) : HasSum (fun n => ↑(n.descFactorial j) * r ^ n) (↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1))
• tsum_descFactorial_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (j : ℕ) {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑(n.descFactorial j) * r ^ n = ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1)
• hasSum_descFactorial_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (j : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun n => ↑(n.descFactorial j) * r ^ n) (↑j.factorial * r ^ j / (1 - r) ^ (j + 1))
• tsum_descFactorial_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (j : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑(n.descFactorial j) * r ^ n = ↑j.factorial * r ^ j / (1 - r) ^ (j + 1)
• hasSum_pow_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (h : ‖r‖ < 1) : HasSum (fun n => ↑n ^ k * r ^ n) (∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1))
• tsum_pow_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ k * r ^ n = ∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1)
• hasSum_pow_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun n => ↑n ^ k * r ^ n) (∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j / (1 - r) ^ (j + 1))
• tsum_pow_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ k * r ^ n = ∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j / (1 - r) ^ (j + 1)
• Real.exp_sub_sum_range_isBigO_pow 📋 Mathlib.Analysis.SpecialFunctions.Exp
  (n : ℕ) : (fun x => Real.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial) =O[nhds 0] fun x => x ^ n
• Complex.exp_sub_sum_range_isBigO_pow 📋 Mathlib.Analysis.SpecialFunctions.Exp
  (n : ℕ) : (fun x => Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i.factorial) =O[nhds 0] fun x => x ^ n
• Real.exp_sub_sum_range_succ_isLittleO_pow 📋 Mathlib.Analysis.SpecialFunctions.Exp
  (n : ℕ) : (fun x => Real.exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial) =o[nhds 0] fun x => x ^ n
• Complex.exp_sub_sum_range_succ_isLittleO_pow 📋 Mathlib.Analysis.SpecialFunctions.Exp
  (n : ℕ) : (fun x => Complex.exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial) =o[nhds 0] fun x => x ^ n
• Nat.doubleFactorial_le_factorial 📋 Mathlib.Data.Nat.Factorial.DoubleFactorial
  (n : ℕ) : n.doubleFactorial ≤ n.factorial
• Nat.factorial_eq_mul_doubleFactorial 📋 Mathlib.Data.Nat.Factorial.DoubleFactorial
  (n : ℕ) : (n + 1).factorial = (n + 1).doubleFactorial * n.doubleFactorial
• Nat.doubleFactorial_two_mul 📋 Mathlib.Data.Nat.Factorial.DoubleFactorial
  (n : ℕ) : (2 * n).doubleFactorial = 2 ^ n * n.factorial
• Nat.multinomial_spec 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} (s : Finset α) (f : α → ℕ) : (∏ i ∈ s, (f i).factorial) * Nat.multinomial s f = (∑ i ∈ s, f i).factorial
• Nat.binomial_eq 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} {f : α → ℕ} {a b : α} [DecidableEq α] (h : a ≠ b) : Nat.multinomial {a, b} f = (f a + f b).factorial / ((f a).factorial * (f b).factorial)
• Nat.binomial_spec 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} {f : α → ℕ} {a b : α} [DecidableEq α] (hab : a ≠ b) : (f a).factorial * (f b).factorial * Nat.multinomial {a, b} f = (f a + f b).factorial
• Nat.multinomial_univ_two 📋 Mathlib.Data.Nat.Choose.Multinomial
  (a b : ℕ) : Nat.multinomial Finset.univ ![a, b] = (a + b).factorial / (a.factorial * b.factorial)
• Nat.multinomial_univ_three 📋 Mathlib.Data.Nat.Choose.Multinomial
  (a b c : ℕ) : Nat.multinomial Finset.univ ![a, b, c] = (a + b + c).factorial / (a.factorial * b.factorial * c.factorial)
• Polynomial.exists_iterate_derivative_eq_factorial_smul 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ (⇑Polynomial.derivative)^[k] p = k.factorial • gp
• Polynomial.aeval_iterate_derivative_of_ge 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) {k : ℕ} (hk : q ≤ k) : ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = q.factorial • (Polynomial.aeval r) gp
• Polynomial.aeval_iterate_derivative_self 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) (r : A) {p' : Polynomial A} (hp : Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p') : (Polynomial.aeval r) ((⇑Polynomial.derivative)^[q] p) = q.factorial • Polynomial.eval r p'
• Polynomial.eval_sumIDeriv_of_pos 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommRing R] [Nontrivial R] [NoZeroDivisors R] (p : Polynomial R) {q : ℕ} (hq : 0 < q) : ∃ gp, gp.natDegree ≤ p.natDegree - q ∧ ∀ (r : R) {p' : Polynomial R}, p = (Polynomial.X - Polynomial.C r) ^ (q - 1) * p' → Polynomial.eval r (Polynomial.sumIDeriv p) = (q - 1).factorial • Polynomial.eval r p' + q.factorial • Polynomial.eval r gp
• Polynomial.aeval_sumIDeriv 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) : ∃ gp, gp.natDegree ≤ p.natDegree - q ∧ ∀ (r : A), (Polynomial.X - Polynomial.C r) ^ q ∣ Polynomial.map (algebraMap R A) p → (Polynomial.aeval r) (Polynomial.sumIDeriv p) = q.factorial • (Polynomial.aeval r) gp
• Polynomial.aeval_sumIDeriv_of_pos 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] [Nontrivial A] [NoZeroDivisors A] (p : Polynomial R) {q : ℕ} (hq : 0 < q) (inj_amap : Function.Injective ⇑(algebraMap R A)) : ∃ gp, gp.natDegree ≤ p.natDegree - q ∧ ∀ (r : A) {p' : Polynomial A}, Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ (q - 1) * p' → (Polynomial.aeval r) (Polynomial.sumIDeriv p) = (q - 1).factorial • Polynomial.eval r p' + q.factorial • (Polynomial.aeval r) gp
• HasFPowerSeriesOnBall.factorial_smul 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) (y : E) [CompleteSpace F] (n : ℕ) : (n.factorial • (p n) fun x => y) = (iteratedFDeriv 𝕜 n f x) fun x => y
• HasFPowerSeriesOnBall.hasSum_iteratedFDeriv 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) [CompleteSpace F] [CharZero 𝕜] {y : E} (hy : y ∈ Metric.eball 0 r) : HasSum (fun n => (↑n.factorial)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) (f (x + y))
• iter_deriv_inv 📋 Mathlib.Analysis.Calculus.Deriv.ZPow
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (x : 𝕜) : deriv^[k] Inv.inv x = (-1) ^ k * ↑k.factorial * x ^ (-1 - ↑k)
• iter_deriv_inv' 📋 Mathlib.Analysis.Calculus.Deriv.ZPow
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) : deriv^[k] Inv.inv = fun x => (-1) ^ k * ↑k.factorial * x ^ (-1 - ↑k)
• iter_deriv_inv_linear 📋 Mathlib.Analysis.Calculus.Deriv.ZPow
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (c d : 𝕜) : (deriv^[k] fun x => (c * x + d)⁻¹) = fun x => (-1) ^ k * ↑k.factorial * c ^ k * (c * x + d) ^ (-1 - ↑k)
• iter_deriv_inv_linear_sub 📋 Mathlib.Analysis.Calculus.Deriv.ZPow
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (c d : 𝕜) : (deriv^[k] fun x => (c * x - d)⁻¹) = fun x => (-1) ^ k * ↑k.factorial * c ^ k * (c * x - d) ^ (-1 - ↑k)
• AnalyticAt.hasFPowerSeriesAt 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (h : AnalyticAt 𝕜 f x) : HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x
• iteratedDeriv_fun_pow_zero 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n m : ℕ} : iteratedDeriv n (fun x => x ^ m) 0 = ↑(if n = m then m.factorial else 0)
• NormedSpace.norm_expSeries_div_summable 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝔸 : Type u_1} [NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] (x : 𝔸) : Summable fun n => ‖x ^ n / ↑n.factorial‖
• NormedSpace.exp_eq_tsum_rat 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝔸 : Type u_2} [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [Algebra ℚ 𝔸] : NormedSpace.exp = fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.exp_eq_ofScalarsSum 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [CharZero 𝕂] : NormedSpace.exp = FormalMultilinearSeries.ofScalarsSum fun n => (↑n.factorial)⁻¹
• NormedSpace.exp_eq_tsum_div 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝔸 : Type u_2} [DivisionRing 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [CharZero 𝔸] : NormedSpace.exp = fun x => ∑' (n : ℕ), x ^ n / ↑n.factorial
• NormedSpace.expSeries_div_summable 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝔸 : Type u_1} [NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Summable fun n => x ^ n / ↑n.factorial
• NormedSpace.exp_eq_tsum 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [CharZero 𝕂] : NormedSpace.exp = fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.expSeries_div_hasSum_exp 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝔸 : Type u_1} [NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp x)
• NormedSpace.norm_expSeries_summable' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) : Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
• NormedSpace.expSeries_summable' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : Summable fun n => (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.expSeries_apply_eq_div 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) (n : ℕ) : ((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n.factorial
• NormedSpace.expSeries_apply_eq_div' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) : (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = fun n => x ^ n / ↑n.factorial
• NormedSpace.expSeries_apply_eq 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) (n : ℕ) : ((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.expSeries_apply_eq' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) : (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = fun n => (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.exp_series_hasSum_exp' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) : HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp x)
• NormedSpace.norm_expSeries_div_summable_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => ‖x ^ n / ↑n.factorial‖
• NormedSpace.norm_expSeries_summable_of_mem_ball' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
• NormedSpace.expSeries_div_summable_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => x ^ n / ↑n.factorial
• NormedSpace.expSeries_summable_of_mem_ball' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.expSeries_hasSum_exp_of_mem_ball' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp x)
• NormedSpace.expSeries_div_hasSum_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp x)
• NormedSpace.expSeries_eq_ofScalars 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) (𝔸 : Type u_2) [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] : NormedSpace.expSeries 𝕂 𝔸 = FormalMultilinearSeries.ofScalars 𝔸 fun n => (↑n.factorial)⁻¹
• NormedSpace.expSeries_sum_eq 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [Ring 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) : (NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.expSeries_sum_eq_div 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [Field 𝕂] [DivisionRing 𝔸] [Algebra 𝕂 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) : (NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), x ^ n / ↑n.factorial
• FloorSemiring.eventually_mul_pow_lt_factorial_sub 📋 Mathlib.Order.Filter.AtTopBot.Floor
  {K : Type u_1} [Ring K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a c : K) (d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < ↑(n - d).factorial
• FloorSemiring.tendsto_pow_div_factorial_atTop 📋 Mathlib.Topology.Algebra.Order.Floor
  {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [TopologicalSpace K] [OrderTopology K] (c : K) : Filter.Tendsto (fun n => c ^ n / ↑n.factorial) Filter.atTop (nhds 0)
• FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop 📋 Mathlib.Topology.Algebra.Order.Floor
  {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [TopologicalSpace K] [OrderTopology K] (a c : K) (d : ℕ) : Filter.Tendsto (fun n => a * c ^ n / ↑(n - d).factorial) Filter.atTop (nhds 0)
• DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ} (h0 : 0 < R) (n : ℕ) (hc : DiffContOnCl ℂ f (Metric.ball c R)) : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
• DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ} (h0 : 0 < R) (n : ℕ) (hc : DifferentiableOn ℂ f (Metric.closedBall c R)) : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
• Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ} {s : Set ℂ} (h0 : 0 < R) (n : ℕ) (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c

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