Loogle!

Result

Found 153 declarations mentioning Polynomial.monomial.

• Polynomial.monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : R →ₗ[R] Polynomial R
• Polynomial.monomial_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Function.Injective ⇑(Polynomial.monomial n)
• Polynomial.ofFinsupp_single 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) : { toFinsupp := AddMonoidAlgebra.single n r } = (Polynomial.monomial n) r
• Polynomial.toFinsupp_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) : ((Polynomial.monomial n) r).toFinsupp = AddMonoidAlgebra.single n r
• Polynomial.erase_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} {a : R} : Polynomial.erase n ((Polynomial.monomial n) a) = 0
• Polynomial.support_monomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).support ⊆ {n}
• Polynomial.support_monomial_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).support ⊆ {n}
• Polynomial.monomial_one_one_eq_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : (Polynomial.monomial 1) 1 = Polynomial.X
• Polynomial.sum_monomial_eq 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : (p.sum fun n a => (Polynomial.monomial n) a) = p
• Polynomial.monomial_zero_right 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.monomial n) 0 = 0
• Polynomial.coeffs_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) {c : R} (hc : c ≠ 0) : ((Polynomial.monomial n) c).coeffs = {c}
• Polynomial.support_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) {a : R} (h : a ≠ 0) : ((Polynomial.monomial n) a).support = {n}
• Polynomial.coeff_monomial_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : ((Polynomial.monomial n) c).coeff n = c
• Polynomial.monomial_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (t : R) (n : ℕ) : (Polynomial.monomial n) t = 0 ↔ t = 0
• Polynomial.monomial_zero_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : (Polynomial.monomial 0) 1 = 1
• Polynomial.induction_on' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R) (add : ∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) (monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)) : motive p
• Polynomial.coeff_monomial_of_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {m n : ℕ} (c : R) (h : m ≠ n) : ((Polynomial.monomial n) c).coeff m = 0
• Polynomial.sum_monomial_index 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S) (hf : f n 0 = 0) : ((Polynomial.monomial n) a).sum f = f n a
• Polynomial.coeff_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {m n : ℕ} [Semiring R] : ((Polynomial.monomial n) a).coeff m = if n = m then a else 0
• Polynomial.monomial_zero_left 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] ⦃a : R⦄ : (Polynomial.monomial 0) a = Polynomial.C a
• Polynomial.X_pow_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.X ^ n = (Polynomial.monomial n) 1
• Polynomial.monomial_one_right_eq_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.monomial n) 1 = Polynomial.X ^ n
• Polynomial.coeff_monomial_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : ((Polynomial.monomial (n + 1)) a).coeff 0 = 0
• Polynomial.monomial_add_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.monomial n) (p.coeff n) + Polynomial.erase n p = p
• Polynomial.C_mul_X_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : Polynomial.C a * Polynomial.X = (Polynomial.monomial 1) a
• Polynomial.smul_X_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] {n : ℕ} : a • Polynomial.X ^ n = (Polynomial.monomial n) a
• Polynomial.C_mul_X_pow_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] {n : ℕ} : Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
• Polynomial.monomial_left_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : R} (ha : a ≠ 0) {i j : ℕ} : (Polynomial.monomial i) a = (Polynomial.monomial j) a ↔ i = j
• Polynomial.mul_eq_sum_sum 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : p * q = ∑ i ∈ p.support, q.sum fun j a => (Polynomial.monomial (i + j)) (p.coeff i * a)
• Polynomial.X_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) : Polynomial.X * (Polynomial.monomial n) r = (Polynomial.monomial (n + 1)) r
• Polynomial.monomial_mul_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) : (Polynomial.monomial n) r * Polynomial.X = (Polynomial.monomial (n + 1)) r
• Polynomial.monomial_eq_monomial_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {m n : ℕ} {a b : R} : (Polynomial.monomial m) a = (Polynomial.monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
• Polynomial.addSubmonoid_closure_setOfPred_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : AddSubmonoid.closure {p | ∃ n a, p = (Polynomial.monomial n) a} = ⊤
• Polynomial.addSubmonoid_closure_setOf_eq_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : AddSubmonoid.closure {p | ∃ n a, p = (Polynomial.monomial n) a} = ⊤
• Polynomial.monomial_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) (k : ℕ) : (Polynomial.monomial n) r ^ k = (Polynomial.monomial (n * k)) (r ^ k)
• Polynomial.smul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (n : ℕ) (b : R) : a • (Polynomial.monomial n) b = (Polynomial.monomial n) (a • b)
• Polynomial.X_pow_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k n : ℕ) (r : R) : Polynomial.X ^ k * (Polynomial.monomial n) r = (Polynomial.monomial (n + k)) r
• Polynomial.monomial_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (r : R) (k : ℕ) : (Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
• Polynomial.C_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} {n : ℕ} [Semiring R] : Polynomial.C a * (Polynomial.monomial n) b = (Polynomial.monomial n) (a * b)
• Polynomial.monomial_mul_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} {n : ℕ} [Semiring R] : (Polynomial.monomial n) a * Polynomial.C b = (Polynomial.monomial n) (a * b)
• Polynomial.lhom_ext' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {f g : Polynomial R →ₗ[R] M} (h : ∀ (n : ℕ), f ∘ₗ Polynomial.monomial n = g ∘ₗ Polynomial.monomial n) : f = g
• Polynomial.lhom_ext'_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {f g : Polynomial R →ₗ[R] M} : f = g ↔ ∀ (n : ℕ), f ∘ₗ Polynomial.monomial n = g ∘ₗ Polynomial.monomial n
• Polynomial.monomial_mul_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n m : ℕ) (r s : R) : (Polynomial.monomial n) r * (Polynomial.monomial m) s = (Polynomial.monomial (n + m)) (r * s)
• Polynomial.monomial_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (n : ℕ) (a : R) : (Polynomial.monomial n) (-a) = -(Polynomial.monomial n) a
• Polynomial.addHom_ext' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} (h : ∀ (n : ℕ), f.comp (Polynomial.monomial n).toAddMonoidHom = g.comp (Polynomial.monomial n).toAddMonoidHom) : f = g
• Polynomial.addHom_ext'_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} : f = g ↔ ∀ (n : ℕ), f.comp (Polynomial.monomial n).toAddMonoidHom = g.comp (Polynomial.monomial n).toAddMonoidHom
• Polynomial.addHom_ext 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} (h : ∀ (n : ℕ) (a : R), f ((Polynomial.monomial n) a) = g ((Polynomial.monomial n) a)) : f = g
• Polynomial.addHom_ext_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} : f = g ↔ ∀ (n : ℕ) (a : R), f ((Polynomial.monomial n) a) = g ((Polynomial.monomial n) a)
• Polynomial.monomial_sub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} [Ring R] (n : ℕ) : (Polynomial.monomial n) (a - b) = (Polynomial.monomial n) a - (Polynomial.monomial n) b
• Polynomial.eval_monomial 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {x : R} {n : ℕ} {a : R} : Polynomial.eval x ((Polynomial.monomial n) a) = a * x ^ n
• Polynomial.eval₂_monomial 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) {n : ℕ} {r : R} : Polynomial.eval₂ f x ((Polynomial.monomial n) r) = f r * x ^ n
• Polynomial.monomial_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ℕ) : ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
• Polynomial.map_monomial 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {n : ℕ} {a : R} : Polynomial.map f ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
• Polynomial.coeff_monomial_zero_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) : ((Polynomial.monomial 0) r * p).coeff d = r * p.coeff d
• Polynomial.coeff_mul_monomial_zero 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (d : ℕ) (r : R) : (p * (Polynomial.monomial 0) r).coeff d = p.coeff d * r
• Polynomial.coeff_monomial_mul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) (r : R) : ((Polynomial.monomial n) r * p).coeff (d + n) = r * p.coeff d
• Polynomial.coeff_mul_monomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] (p : Polynomial R) (n d : ℕ) (r : R) : (p * (Polynomial.monomial n) r).coeff (d + n) = p.coeff d * r
• Polynomial.leadingCoeff_monomial 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : ((Polynomial.monomial n) a).leadingCoeff = a
• Polynomial.natDegree_monomial_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (a : R) {m : ℕ} : ((Polynomial.monomial m) a).natDegree ≤ m
• Polynomial.degree_monomial_le 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).degree ≤ ↑n
• Polynomial.natDegree_monomial_eq 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] (i : ℕ) {r : R} (r0 : r ≠ 0) : ((Polynomial.monomial i) r).natDegree = i
• Polynomial.degree_monomial 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) : ((Polynomial.monomial n) a).degree = ↑n
• Polynomial.natDegree_monomial 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} [Semiring R] [DecidableEq R] (i : ℕ) (r : R) : ((Polynomial.monomial i) r).natDegree = if r = 0 then 0 else i
• Polynomial.as_sum_support 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i)
• Polynomial.as_sum_range' 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (hn : p.natDegree < n) : p = ∑ i ∈ Finset.range n, (Polynomial.monomial i) (p.coeff i)
• Polynomial.as_sum_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), (Polynomial.monomial i) (p.coeff 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.card_support_le_one_iff_monomial 📋 Mathlib.Algebra.Polynomial.Monomial
  {R : Type u} [Semiring R] {f : Polynomial R} : f.support.card ≤ 1 ↔ ∃ n a, f = (Polynomial.monomial n) a
• Polynomial.monomial_one_eq_iff 📋 Mathlib.Algebra.Polynomial.Monomial
  {R : Type u} [Semiring R] [Nontrivial R] {i j : ℕ} : (Polynomial.monomial i) 1 = (Polynomial.monomial j) 1 ↔ i = j
• Polynomial.aeval_monomial 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} {r : R} : (Polynomial.aeval x) ((Polynomial.monomial n) r) = (algebraMap R A) r * x ^ n
• Polynomial.mapAlgHom_monomial 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (n : ℕ) (a : A) : (Polynomial.mapAlgHom f) ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
• Polynomial.X_pow_smul_rTensor_monomial 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {N : Type u_3} [AddCommMonoid N] [Module R N] (k : ℕ) (sn : TensorProduct R S N) : Polynomial.X ^ k • (LinearMap.rTensor N (↑R (Polynomial.monomial 0))) sn = (LinearMap.rTensor N (↑R (Polynomial.monomial k))) sn
• MvPolynomial.pUnitAlgEquiv_monomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) [CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R} : (MvPolynomial.pUnitAlgEquiv R) ((MvPolynomial.monomial d) r) = (Polynomial.monomial (d ())) r
• MvPolynomial.uniqueAlgEquiv_monomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] [Unique σ] {d : σ →₀ ℕ} {r : R} : (MvPolynomial.uniqueAlgEquiv R σ) ((MvPolynomial.monomial d) r) = (Polynomial.monomial (d default)) r
• MvPolynomial.pUnitAlgEquiv_symm_monomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) [CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R} : (MvPolynomial.pUnitAlgEquiv R).symm ((Polynomial.monomial (d ())) r) = (MvPolynomial.monomial d) r
• MvPolynomial.uniqueAlgEquiv_symm_monomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] [Unique σ] {d : σ →₀ ℕ} {r : R} : (MvPolynomial.uniqueAlgEquiv R σ).symm ((Polynomial.monomial (d default)) r) = (MvPolynomial.monomial d) r
• MvPolynomial.optionEquivLeft_monomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) (S₁ : Type v) [CommSemiring R] (m : Option S₁ →₀ ℕ) (r : R) : (MvPolynomial.optionEquivLeft R S₁) ((MvPolynomial.monomial m) r) = (Polynomial.monomial (m none)) ((MvPolynomial.monomial m.some) r)
• Polynomial.natTrailingDegree_monomial_le 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : ((Polynomial.monomial n) a).natTrailingDegree ≤ n
• Polynomial.le_trailingDegree_monomial 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : ↑n ≤ ((Polynomial.monomial n) a).trailingDegree
• Polynomial.natTrailingDegree_monomial 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {a : R} {n : ℕ} [Semiring R] (ha : a ≠ 0) : ((Polynomial.monomial n) a).natTrailingDegree = n
• Polynomial.trailingDegree_monomial 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} {a : R} {n : ℕ} [Semiring R] (ha : a ≠ 0) : ((Polynomial.monomial n) a).trailingDegree = ↑n
• Polynomial.monomial_natDegree_leadingCoeff_eq_self 📋 Mathlib.Algebra.Polynomial.Degree.Monomial
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : (Polynomial.monomial p.natDegree) p.leadingCoeff = p
• Polynomial.eraseLead_monomial 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] (i : ℕ) (r : R) : ((Polynomial.monomial i) r).eraseLead = 0
• Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.eraseLead + (Polynomial.monomial f.natDegree) f.leadingCoeff = f
• Polynomial.self_sub_monomial_natDegree_leadingCoeff 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_2} [Ring R] (f : Polynomial R) : f - (Polynomial.monomial f.natDegree) f.leadingCoeff = f.eraseLead
• Polynomial.map_natDegree_eq_natDegree 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F} (p : Polynomial R) (φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n) : (φ p).natDegree = p.natDegree
• Polynomial.map_natDegree_eq_sub 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F} {p : Polynomial R} {k : ℕ} (φ_k : ∀ (f : Polynomial R), f.natDegree < k → φ f = 0) (φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n - k) : (φ p).natDegree = p.natDegree - k
• Polynomial.mono_map_natDegree_eq 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F} {p : Polynomial R} (k : ℕ) (fu : ℕ → ℕ) (fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0) (fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m) (φ_k : ∀ {f : Polynomial R}, f.natDegree < k → φ f = 0) (φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = fu n) : (φ p).natDegree = fu p.natDegree
• Polynomial.monomial_coe_mem_degreeLT 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} (i : Fin n) (a : R) : (Polynomial.monomial ↑i) a ∈ Polynomial.degreeLT R n
• Polynomial.derivative_monomial 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : Polynomial.derivative ((Polynomial.monomial n) a) = (Polynomial.monomial (n - 1)) (a * ↑n)
• Polynomial.derivative_monomial_succ 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : Polynomial.derivative ((Polynomial.monomial (n + 1)) a) = (Polynomial.monomial n) (a * (↑n + 1))
• Polynomial.natDegree_ne_zero_induction_on 📋 Mathlib.Algebra.Polynomial.Inductions
  {R : Type u} [Semiring R] {M : Polynomial R → Prop} {f : Polynomial R} (f0 : f.natDegree ≠ 0) (h_C_add : ∀ {a : R} {p : Polynomial R}, M p → M (Polynomial.C a + p)) (h_add : ∀ {p q : Polynomial R}, M p → M q → M (p + q)) (h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((Polynomial.monomial n) a)) : M f
• Polynomial.sum_modByMonic_coeff 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ ↑n) : ∑ i, (Polynomial.monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
• Polynomial.expand_monomial 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p q : ℕ) (r : R) : (Polynomial.expand R p) ((Polynomial.monomial q) r) = (Polynomial.monomial (q * p)) r
• Polynomial.roots_monomial 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a ≠ 0) (n : ℕ) : ((Polynomial.monomial n) a).roots = n • {0}
• Polynomial.aroots_monomial 📋 Mathlib.Algebra.Polynomial.Roots
  {S : Type v} {T : Type w} [CommRing T] [IsDomain T] [CommRing S] [IsDomain S] [Algebra T S] [Module.IsTorsionFree T S] {a : T} (ha : a ≠ 0) (n : ℕ) : ((Polynomial.monomial n) a).aroots S = n • {0}
• Polynomial.rootSet_monomial 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) : ((Polynomial.monomial n) a).rootSet S = {0}
• Polynomial.content_monomial 📋 Mathlib.RingTheory.Polynomial.Content
  {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {r : R} {k : ℕ} : ((Polynomial.monomial k) r).content = normalize r
• PolyEquivTensor.toFunAlgHom_apply_tmul 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
• polyEquivTensor_symm_apply_tmul 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
• PolyEquivTensor.invFun_monomial 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) (a : A) : PolyEquivTensor.invFun R A ((Polynomial.monomial n) a) = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] Polynomial.X ^ n
• PolyEquivTensor.toFunBilinear_apply_eq_sum 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ((PolyEquivTensor.toFunBilinear R A) a) p = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
• Polynomial.toLaurent_C_mul_T 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] (n : ℕ) (r : R) : Polynomial.toLaurent ((Polynomial.monomial n) r) = LaurentPolynomial.C r * LaurentPolynomial.T ↑n
• LaurentPolynomial.trunc_C_mul_T 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] (n : ℤ) (r : R) : LaurentPolynomial.trunc (LaurentPolynomial.C r * LaurentPolynomial.T n) = if 0 ≤ n then (Polynomial.monomial n.toNat) r else 0
• matPolyEquiv_coeff_apply_aux_1 📋 Mathlib.RingTheory.MatrixPolynomialAlgebra
  {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (i j : n) (k : ℕ) (x : R) : matPolyEquiv (Matrix.single i j ((Polynomial.monomial k) x)) = (Polynomial.monomial k) (Matrix.single i j x)
• Polynomial.isNilpotent_monomial_iff 📋 Mathlib.RingTheory.Polynomial.Nilpotent
  {R : Type u_1} {r : R} [Semiring R] {n : ℕ} : IsNilpotent ((Polynomial.monomial n) r) ↔ IsNilpotent r
• Polynomial.monomial_mem_lifts 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {s : S} (n : ℕ) (h : s ∈ Set.range ⇑f) : (Polynomial.monomial n) s ∈ Polynomial.lifts f
• Polynomial.monomial_mem_lifts_and_degree_eq 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {s : S} {n : ℕ} (hl : (Polynomial.monomial n) s ∈ Polynomial.lifts f) : ∃ q, Polynomial.map f q = (Polynomial.monomial n) s ∧ q.degree = ((Polynomial.monomial n) s).degree
• 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.taylor_monomial 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [Semiring R] (r : R) (i : ℕ) (k : R) : (Polynomial.taylor r) ((Polynomial.monomial i) k) = Polynomial.C k * (Polynomial.X + Polynomial.C r) ^ i
• Polynomial.Splits.monomial 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).Splits
• PolynomialModule.monomial_smul_single 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (j : ℕ) (m : M) : (Polynomial.monomial i) r • PolynomialModule.single R j m = PolynomialModule.single R (i + j) (r • m)
• PolynomialModule.monomial_smul_apply 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (g : PolynomialModule R M) (n : ℕ) : ((Polynomial.monomial i) r • g).coeff n = if i ≤ n then r • g.coeff (n - i) else 0
• PolynomialModule.monomial_smul_lsingle 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (j : ℕ) (m : M) : (Polynomial.monomial i) r • (PolynomialModule.lsingle R j) m = (PolynomialModule.lsingle R (i + j)) (r • m)
• PolynomialModule.equivPolynomial_single 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} [CommRing R] {S : Type u_6} [CommRing S] [Algebra R S] (n : ℕ) (x : S) : PolynomialModule.equivPolynomial (PolynomialModule.single R n x) = (Polynomial.monomial n) x
• PolynomialModule.equivPolynomial_symm_monomial 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} [CommRing R] {S : Type u_6} [CommRing S] [Algebra R S] (n : ℕ) (x : S) : PolynomialModule.equivPolynomial.symm ((Polynomial.monomial n) x) = PolynomialModule.single R n x
• adjoin_monomial_eq_reesAlgebra 📋 Mathlib.RingTheory.ReesAlgebra
  {R : Type u} [CommRing R] (I : Ideal R) : Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I) = reesAlgebra I
• reesAlgebra.monomial_mem 📋 Mathlib.RingTheory.ReesAlgebra
  {R : Type u} [CommRing R] {I : Ideal R} {i : ℕ} {r : R} : (Polynomial.monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i
• monomial_mem_adjoin_monomial 📋 Mathlib.RingTheory.ReesAlgebra
  {R : Type u} [CommRing R] {I : Ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) : (Polynomial.monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I)
• AdjoinRoot.powerBasisAux'_repr_symm_apply 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (c : Fin g.natDegree →₀ R) : (AdjoinRoot.powerBasisAux' hg).repr.symm c = (AdjoinRoot.mk g) (∑ i, (Polynomial.monomial ↑i) (c i))
• Polynomial.coe_basisMonomials 📋 Mathlib.Algebra.Polynomial.Basis
  (R : Type u) [Semiring R] : ⇑(Polynomial.basisMonomials R) = fun s => (Polynomial.monomial s) 1
• Derivation.mapCoeffs_monomial 📋 Mathlib.RingTheory.Derivation.MapCoeffs
  {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] (d : Derivation R A M) (n : ℕ) (x : A) : d.mapCoeffs ((Polynomial.monomial n) x) = PolynomialModule.single A n (d x)
• Differential.mapCoeffs_monomial 📋 Mathlib.RingTheory.Derivation.MapCoeffs
  {A : Type u_1} [CommRing A] [Differential A] (n : ℕ) (x : A) : Differential.mapCoeffs ((Polynomial.monomial n) x) = (Polynomial.monomial n) x′
• Polynomial.Bivariate.swap_monomial 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} [CommSemiring R] (n : ℕ) (f : Polynomial R) : Polynomial.Bivariate.swap ((Polynomial.monomial n) f) = Polynomial.map Polynomial.C f * Polynomial.C (Polynomial.X ^ n)
• Polynomial.Bivariate.swap_monomial_monomial 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} [CommSemiring R] (n m : ℕ) (r : R) : Polynomial.Bivariate.swap ((Polynomial.monomial n) ((Polynomial.monomial m) r)) = (Polynomial.monomial m) ((Polynomial.monomial n) r)
• Polynomial.coeffList_monomial 📋 Mathlib.Algebra.Polynomial.CoeffList
  {R : Type u_1} [Semiring R] {x : R} (hx : x ≠ 0) (n : ℕ) : ((Polynomial.monomial n) x).coeffList = x :: List.replicate n 0
• Polynomial.isMonicOfDegree_monomial_one 📋 Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
  {R : Type u_1} [Semiring R] [Nontrivial R] (n : ℕ) : ((Polynomial.monomial n) 1).IsMonicOfDegree n
• Polynomial.homogenize_monomial_of_lt 📋 Mathlib.Algebra.Polynomial.Homogenize
  {R : Type u_1} [CommSemiring R] {m n : ℕ} (h : n < m) (r : R) : ((Polynomial.monomial m) r).homogenize n = 0
• Polynomial.homogenize_monomial 📋 Mathlib.Algebra.Polynomial.Homogenize
  {R : Type u_1} [CommSemiring R] {m n : ℕ} (h : m ≤ n) (r : R) : ((Polynomial.monomial m) r).homogenize n = (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r
• Polynomial.mirror_monomial 📋 Mathlib.Algebra.Polynomial.Mirror
  {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).mirror = (Polynomial.monomial n) a
• Polynomial.ofFn_eq_sum_monomial 📋 Mathlib.Algebra.Polynomial.OfFn
  {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} (v : Fin n → R) : (Polynomial.ofFn n) v = ∑ i, (Polynomial.monomial ↑i) (v i)
• Polynomial.signVariations_monomial 📋 Mathlib.Algebra.Polynomial.RuleOfSigns
  {R : Type u_1} [Semiring R] [LinearOrder R] (d : ℕ) (c : R) : ((Polynomial.monomial d) c).signVariations = 0
• Polynomial.succ_signVariations_X_sub_C_mul_monomial 📋 Mathlib.Algebra.Polynomial.RuleOfSigns
  {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {η : R} {d : ℕ} {c : R} (hc : c ≠ 0) (hη : 0 < η) : ((Polynomial.monomial d) c).signVariations + 1 ≤ ((Polynomial.X - Polynomial.C η) * (Polynomial.monomial d) c).signVariations
• Polynomial.smeval_monomial 📋 Mathlib.Algebra.Polynomial.Smeval
  {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [MulActionWithZero R S] (x : S) (n : ℕ) : ((Polynomial.monomial n) r).smeval x = r • x ^ n
• Polynomial.smeval_monomial_mul 📋 Mathlib.Algebra.Polynomial.Smeval
  (R : Type u_1) [Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ℕ) : ((Polynomial.monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)
• Polynomial.coe_monomial 📋 Mathlib.RingTheory.PowerSeries.Basic
  {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ↑((Polynomial.monomial n) a) = (PowerSeries.monomial n) a
• PowerSeries.trunc_apply 📋 Mathlib.RingTheory.PowerSeries.Trunc
  {R : Type u_1} [Semiring R] (n : ℕ) (φ : PowerSeries R) : (PowerSeries.trunc n) φ = ∑ m ∈ Finset.Ico 0 n, (Polynomial.monomial m) ((PowerSeries.coeff m) φ)
• PowerSeries.trunc_succ 📋 Mathlib.RingTheory.PowerSeries.Trunc
  {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) : (PowerSeries.trunc n.succ) f = (PowerSeries.trunc n) f + (Polynomial.monomial n) ((PowerSeries.coeff n) f)
• Polynomial.valuation_aeval_monomial_eq_valuation_pow 📋 Mathlib.RingTheory.Valuation.IsTrivialOn
  {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [CommSemiring A] {B : Type u_3} [Ring B] [Algebra A B] {v : Valuation B Γ} [hv : Valuation.IsTrivialOn A v] (w : B) (n : ℕ) {a : A} (ha : a ≠ 0) : v ((Polynomial.aeval w) ((Polynomial.monomial n) a)) = v w ^ n
• RatFunc.algebraMap_monomial 📋 Mathlib.FieldTheory.RatFunc.AsPolynomial
  {K : Type u} [CommRing K] [IsDomain K] (n : ℕ) (a : K) : (algebraMap (Polynomial K) (RatFunc K)) ((Polynomial.monomial n) a) = RatFunc.C a * RatFunc.X ^ n
• Polynomial.valuation_monomial_eq_valuation_X_pow 📋 Mathlib.FieldTheory.RatFunc.AsPolynomial
  (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K} (ha : a ≠ 0) : v ↑((Polynomial.monomial n) a) = v RatFunc.X ^ n
• Polynomial.valuation_inv_monomial_eq_valuation_X_zpow 📋 Mathlib.FieldTheory.RatFunc.AsPolynomial
  (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [hv : Valuation.IsTrivialOn K v] (n : ℕ) {a : K} (ha : a ≠ 0) : v (1 / ↑((Polynomial.monomial n) a)) = v RatFunc.X ^ (-↑n)
• Polynomial.toAddCircle_monomial_eq_smul_fourier 📋 Mathlib.Analysis.Polynomial.Fourier
  {n : ℕ} {c : ℂ} : Polynomial.toAddCircle ((Polynomial.monomial n) c) = c • fourier ↑n
• Polynomial.gaussNorm_monomial 📋 Mathlib.RingTheory.Polynomial.GaussNorm
  {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) [ZeroHomClass F R ℝ] (n : ℕ) (r : R) : Polynomial.gaussNorm v c ((Polynomial.monomial n) r) = v r * c ^ n
• Polynomial.supNorm_monomial 📋 Mathlib.Analysis.Polynomial.Norm
  {A : Type u_1} [SeminormedRing A] (n : ℕ) {a : A} : ((Polynomial.monomial n) a).supNorm = ‖a‖
• Polynomial.logMahlerMeasure_monomial 📋 Mathlib.Analysis.Polynomial.MahlerMeasure
  (n : ℕ) (z : ℂ) : ((Polynomial.monomial n) z).logMahlerMeasure = Real.log ‖z‖
• Polynomial.bernoulli_def 📋 Mathlib.NumberTheory.BernoulliPolynomials
  (n : ℕ) : Polynomial.bernoulli n = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (bernoulli (n - i) * ↑(n.choose i))
• Polynomial.sum_bernoulli 📋 Mathlib.NumberTheory.BernoulliPolynomials
  (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ↑((n + 1).choose k) • Polynomial.bernoulli k = (Polynomial.monomial n) (↑n + 1)
• Polynomial.contentIdeal_monomial 📋 Mathlib.RingTheory.Polynomial.ContentIdeal
  {R : Type u_1} [Semiring R] (n : ℕ) (r : R) : ((Polynomial.monomial n) r).contentIdeal = Ideal.span {r}
• Polynomial.opRingEquiv_op_monomial 📋 Mathlib.RingTheory.Polynomial.Opposites
  {R : Type u_1} [Semiring R] (n : ℕ) (r : R) : (Polynomial.opRingEquiv R) (MulOpposite.op ((Polynomial.monomial n) r)) = (Polynomial.monomial n) (MulOpposite.op r)
• Polynomial.opRingEquiv_symm_monomial 📋 Mathlib.RingTheory.Polynomial.Opposites
  {R : Type u_1} [Semiring R] (n : ℕ) (r : Rᵐᵒᵖ) : (Polynomial.opRingEquiv R).symm ((Polynomial.monomial n) r) = MulOpposite.op ((Polynomial.monomial n) (MulOpposite.unop r))
• Mathlib.Tactic.Polynomial.monomial_eq_smul 📋 Mathlib.Tactic.Polynomial.Basic
  {R : Type u_1} [CommSemiring R] (a : R) (n : ℕ) : (Polynomial.monomial n) a = a • Polynomial.X ^ n

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 ce5dd8c