Loogle!

Result

Found 5960 declarations mentioning Polynomial. Of these, only the first 200 are shown.

• Polynomial 📋 Mathlib.Algebra.Polynomial.Basic
  (R : Type u_1) [Semiring R] : Type u_1
• Polynomial.X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial R
• Polynomial.inhabited 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Inhabited (Polynomial R)
• Polynomial.instAdd 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Add (Polynomial R)
• Polynomial.instMul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Mul (Polynomial R)
• Polynomial.instNatCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : NatCast (Polynomial R)
• Polynomial.instOne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : One (Polynomial R)
• Polynomial.instZero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Zero (Polynomial R)
• Polynomial.semiring 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Semiring (Polynomial R)
• Polynomial.coeff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial R → ℕ → R
• Polynomial.coeffs 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : Finset R
• Polynomial.instNSMul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : SMul ℕ (Polynomial R)
• Polynomial.pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Pow (Polynomial R) ℕ
• Polynomial.support 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial R → Finset ℕ
• Polynomial.commSemiring 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [CommSemiring R] : CommSemiring (Polynomial R)
• Polynomial.instDecidableEq 📋 Mathlib.Algebra.Polynomial.Basic
  (R : Type u) [Semiring R] [DecidableEq R] : DecidableEq (Polynomial R)
• Polynomial.instIntCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] : IntCast (Polynomial R)
• Polynomial.instNeg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] : Neg (Polynomial R)
• Polynomial.instSub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] : Sub (Polynomial R)
• Polynomial.nontrivial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] : Nontrivial (Polynomial R)
• Polynomial.ring 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] : Ring (Polynomial R)
• Polynomial.unique 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Subsingleton R] : Unique (Polynomial R)
• Polynomial.erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u_1} [Semiring R] (n : ℕ) : Polynomial R → Polynomial R
• Polynomial.instZSMul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] : SMul ℤ (Polynomial R)
• Polynomial.nontrivial_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Nontrivial (Polynomial R) ↔ Nontrivial R
• Polynomial.ofFinsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u_1} [Semiring R] (toFinsupp : AddMonoidAlgebra R ℕ) : Polynomial R
• Polynomial.subsingleton_iff_subsingleton 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Subsingleton (Polynomial R) ↔ Subsingleton R
• Polynomial.toFinsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u_1} [Semiring R] (self : Polynomial R) : AddMonoidAlgebra R ℕ
• Polynomial.commRing 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [CommRing R] : CommRing (Polynomial R)
• Polynomial.repr 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Repr R] [DecidableEq R] : Repr (Polynomial R)
• Polynomial.update 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : Polynomial R
• Polynomial.coeff_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Function.Injective Polynomial.coeff
• Polynomial.sum 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S) : S
• Polynomial.toFinsupp_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Function.Injective Polynomial.toFinsupp
• Polynomial.finite_range_coeff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (f : Polynomial R) : (Set.range f.coeff).Finite
• Polynomial.commute_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : Commute Polynomial.X p
• Polynomial.Nontrivial.of_polynomial_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} (h : p ≠ q) : Nontrivial R
• Polynomial.C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : R →+* Polynomial R
• Polynomial.eta 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (f : Polynomial R) : { toFinsupp := f.toFinsupp } = f
• Polynomial.coeff_update_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p.update n a).coeff n = a
• Polynomial.forall_eq_iff_forall_eq 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : (∀ (f g : Polynomial R), f = g) ↔ ∀ (a b : R), a = b
• Polynomial.forall_iff_forall_finsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (P : Polynomial R → Prop) : (∀ (p : Polynomial R), P p) ↔ ∀ (q : AddMonoidAlgebra R ℕ), P { toFinsupp := q }
• Polynomial.X_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X ≠ 0
• Polynomial.instIsDomainOfIsCancelAdd 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [IsCancelAdd R] [IsDomain R] : IsDomain (Polynomial R)
• Polynomial.smulZeroClass 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] : SMulZeroClass S (Polynomial R)
• Polynomial.coeffs_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.coeffs 0 = ∅
• Polynomial.support_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.erase n p).support = p.support.erase n
• Polynomial.support_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.support 0 = ∅
• Polynomial.coeff_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : p.coeff = q.coeff ↔ p = q
• Polynomial.erase_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n i : ℕ) (h : i ≠ n) : (Polynomial.erase n p).coeff i = p.coeff i
• Polynomial.ext 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
• Polynomial.coeffs.eq_1 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : p.coeffs = Finset.image (fun n => p.coeff n) p.support
• Polynomial.ext_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
• Polynomial.support_toFinsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : p.toFinsupp.support = p.support
• Polynomial.toFinsupp_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a b : Polynomial R} : a.toFinsupp = b.toFinsupp ↔ a = b
• Polynomial.coeff_update_ne 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) : (p.update n a).coeff i = p.coeff i
• Polynomial.coeffs_nonempty_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeffs.Nonempty ↔ p ≠ 0
• Polynomial.support_nonempty 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support.Nonempty ↔ p ≠ 0
• Polynomial.coeff_update 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (p.update n a).coeff = Function.update p.coeff n a
• Polynomial.exists_iff_exists_finsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (P : Polynomial R → Prop) : (∃ p, P p) ↔ ∃ q, P { toFinsupp := q }
• Polynomial.ofFinsupp_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a b : AddMonoidAlgebra R ℕ} : { toFinsupp := a } = { toFinsupp := b } ↔ a = b
• Polynomial.erase_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.erase n p).coeff n = 0
• Polynomial.support_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] {p : Polynomial R} : (-p).support = p.support
• Polynomial.ofFinsupp.injEq 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u_1} [Semiring R] (toFinsupp toFinsupp✝ : AddMonoidAlgebra R ℕ) : ({ toFinsupp := toFinsupp } = { toFinsupp := toFinsupp✝ }) = (toFinsupp = toFinsupp✝)
• Polynomial.instNoZeroDivisors 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (Polynomial R)
• Polynomial.noZeroDivisors_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : NoZeroDivisors (Polynomial R) ↔ NoZeroDivisors R
• Polynomial.update_zero_eq_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : p.update n 0 = Polynomial.erase n p
• Polynomial.coeff_update_apply 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) (i : ℕ) : (p.update n a).coeff i = if i = n then a else p.coeff i
• Polynomial.coeff_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.coeff 0 n = 0
• Polynomial.coeffs_empty_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.coeffs = ∅ ↔ p = 0
• Polynomial.erase_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.erase n 0 = 0
• Polynomial.support_eq_empty 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support = ∅ ↔ p = 0
• Polynomial.card_support_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support.card = 0 ↔ p = 0
• Polynomial.ofFinsupp_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) (n : ℕ) : { toFinsupp := Finsupp.erase n p } = Polynomial.erase n { toFinsupp := p }
• Polynomial.sum_def 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
• Polynomial.toFinsuppIso 📋 Mathlib.Algebra.Polynomial.Basic
  (R : Type u) [Semiring R] : Polynomial R ≃+* AddMonoidAlgebra R ℕ
• Polynomial.toFinsupp_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
• Polynomial.sum.eq_1 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
• Polynomial.module 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] [Module S R] : Module S (Polynomial R)
• Polynomial.coeff_one_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.coeff 1 0 = 1
• Polynomial.update.eq_1 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : p.update n a = { toFinsupp := Finsupp.update p.toFinsupp n a }
• Polynomial.mem_support_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : n ∈ p.support ↔ p.coeff n ≠ 0
• Polynomial.ofFinsupp_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : { toFinsupp := 1 } = 1
• Polynomial.support_update_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (p.update n 0).support = p.support.erase n
• Polynomial.notMem_support_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : n ∉ p.support ↔ p.coeff n = 0
• Polynomial.toFinsupp_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.toFinsupp 1 = 1
• Polynomial.mem_coeffs_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n
• Polynomial.coeff_mem_coeffs 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs
• Polynomial.coeffs_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.coeffs 1 ⊆ {1}
• Polynomial.sum_zero_index 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (f : ℕ → R → S) : Polynomial.sum 0 f = 0
• Polynomial.distribMulAction 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] : DistribMulAction S (Polynomial R)
• Polynomial.instIsCancelMulZeroOfIsCancelAdd 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [IsCancelAdd R] [IsCancelMulZero R] : IsCancelMulZero (Polynomial R)
• Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R] : IsLeftCancelMulZero (Polynomial R)
• Polynomial.instIsRightCancelMulZeroOfIsCancelAdd 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R] : IsRightCancelMulZero (Polynomial R)
• Polynomial.ofMultiset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [CommRing R] : AddChar (Multiset R) (Polynomial R)
• Polynomial.distribSMul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [DistribSMul S R] : DistribSMul S (Polynomial R)
• Polynomial.ofFinsupp.sizeOf_spec 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u_1} [Semiring R] [SizeOf R] (toFinsupp : AddMonoidAlgebra R ℕ) : sizeOf { toFinsupp := toFinsupp } = 1 + sizeOf toFinsupp
• Polynomial.C_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Function.Injective ⇑Polynomial.C
• Polynomial.coeff_erase 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n i : ℕ) : (Polynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
• Polynomial.coeff_ofNat_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : ℕ) [a.AtLeastTwo] : (OfNat.ofNat a).coeff 0 = OfNat.ofNat a
• Polynomial.commute_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : Commute (Polynomial.X ^ n) p
• Polynomial.erase_def 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u_1} [Semiring R] (n : ℕ) (x✝ : Polynomial R) : Polynomial.erase n x✝ = match x✝ with | { toFinsupp := p } => { toFinsupp := Finsupp.erase n p }
• Polynomial.ofFinsupp_natCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : { toFinsupp := ↑n } = ↑n
• Polynomial.toFinsupp_apply 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (f : Polynomial R) (i : ℕ) : f.toFinsupp i = f.coeff i
• Polynomial.ofFinsupp_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : { toFinsupp := 0 } = 0
• Polynomial.toFinsupp_natCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (↑n).toFinsupp = ↑n
• Polynomial.coeff_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (p : Polynomial R) (n : ℕ) : (-p).coeff n = -p.coeff n
• Polynomial.support_update_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) {a : R} (ha : a ≠ 0) : (p.update n a).support = insert n p.support
• Polynomial.toFinsupp_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.toFinsupp 0 = 0
• Polynomial.faithfulSMul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [FaithfulSMul S R] : FaithfulSMul S (Polynomial R)
• Polynomial.support_add 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : (p + q).support ⊆ p.support ∪ q.support
• Polynomial.monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : R →ₗ[R] Polynomial R
• Polynomial.toFinsupp_eq_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : Polynomial R} : a.toFinsupp = 1 ↔ a = 1
• Polynomial.X_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.X * p = p * Polynomial.X
• Polynomial.ofFinsupp_eq_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : AddMonoidAlgebra R ℕ} : { toFinsupp := a } = 1 ↔ a = 1
• Polynomial.ofFinsupp_intCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (z : ℤ) : { toFinsupp := ↑z } = ↑z
• IsSMulRegular.polynomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {a : S} (ha : IsSMulRegular R a) : IsSMulRegular (Polynomial R) a
• Polynomial.X_ne_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] (a : R) : Polynomial.X ≠ Polynomial.C a
• Polynomial.coeff_natCast_ite 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {m n : ℕ} [Semiring R] : (↑m).coeff n = ↑(if n = 0 then m else 0)
• Polynomial.eq_zero_of_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (h : 0 = 1) (p : Polynomial R) : p = 0
• Polynomial.toFinsupp_intCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (z : ℤ) : (↑z).toFinsupp = ↑z
• Polynomial.coeff_ofNat_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a n : ℕ) [h : a.AtLeastTwo] : (OfNat.ofNat a).coeff (n + 1) = 0
• Polynomial.coeff_C_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : (Polynomial.C a).coeff 0 = a
• Polynomial.natCast_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (p : Polynomial R) : ↑n * p = n • p
• Polynomial.ofFinsupp_sum 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → AddMonoidAlgebra R ℕ) : { toFinsupp := ∑ i ∈ s, f i } = ∑ i ∈ s, { toFinsupp := f i }
• Polynomial.toFinsupp_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : Polynomial R} : a.toFinsupp = 0 ↔ a = 0
• Polynomial.toFinsupp_sum 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) : (∑ i ∈ s, f i).toFinsupp = ∑ i ∈ s, (f i).toFinsupp
• Polynomial.ofFinsupp_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : AddMonoidAlgebra R ℕ} : { toFinsupp := a } = 0 ↔ a = 0
• Polynomial.toFinsupp_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).toFinsupp = AddMonoidAlgebra.single 0 a
• Polynomial.ofFinsupp_ofNat 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : { toFinsupp := OfNat.ofNat n } = OfNat.ofNat n
• Polynomial.support_C_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).support ⊆ {0}
• Polynomial.toFinsupp_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).toFinsupp = AddMonoidAlgebra.single n 1
• Polynomial.toFinsupp_ofNat 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).toFinsupp = OfNat.ofNat n
• Polynomial.instNoZeroSMulDivisors 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] : NoZeroSMulDivisors S (Polynomial R)
• Polynomial.C_eq_natCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.C ↑n = ↑n
• Polynomial.coeff_one 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} : Polynomial.coeff 1 n = if n = 0 then 1 else 0
• Polynomial.toFinsuppIsoLinear 📋 Mathlib.Algebra.Polynomial.Basic
  (R : Type u) [Semiring R] : Polynomial R ≃ₗ[R] AddMonoidAlgebra R ℕ
• Polynomial.toFinsupp_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a b : Polynomial R) : (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
• Polynomial.ofFinsupp_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a b : AddMonoidAlgebra R ℕ) : { toFinsupp := a * b } = { toFinsupp := a } * { toFinsupp := b }
• Polynomial.sum_add 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f g : ℕ → R → S) : (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g
• Polynomial.C_0 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.C 0 = 0
• Polynomial.C_1 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.C 1 = 1
• Polynomial.coeff_C_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] (h : n ≠ 0) : (Polynomial.C a).coeff n = 0
• Polynomial.ofFinsupp_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : AddMonoidAlgebra R ℕ) (n : ℕ) : { toFinsupp := a ^ n } = { toFinsupp := a } ^ n
• Polynomial.toFinsupp_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : Polynomial R) (n : ℕ) : (a ^ n).toFinsupp = a.toFinsupp ^ n
• Polynomial.coeff_C_succ 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {r : R} {n : ℕ} : (Polynomial.C r).coeff (n + 1) = 0
• Polynomial.toFinsupp_add 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a b : Polynomial R) : (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
• Polynomial.C_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : Polynomial.C a = 0 ↔ a = 0
• Polynomial.C_ne_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} [Semiring R] : Polynomial.C a ≠ 0 ↔ a ≠ 0
• Polynomial.coeff_sub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (p q : Polynomial R) (n : ℕ) : (p - q).coeff n = p.coeff n - q.coeff n
• Polynomial.ofFinsupp_add 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a b : AddMonoidAlgebra R ℕ} : { toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }
• Polynomial.support_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : R} (h : a ≠ 0) : (Polynomial.C a).support = {0}
• Polynomial.sum_eq_of_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {p : Polynomial R} (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {s : Finset ℕ} (hs : p.support ⊆ s) : p.sum f = ∑ n ∈ s, f n (p.coeff n)
• Polynomial.support_update 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) [Decidable (a = 0)] : (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
• Polynomial.C_ofNat 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : Polynomial.C (OfNat.ofNat n) = OfNat.ofNat n
• Polynomial.support_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (H : ¬1 = 0) (n : ℕ) : (Polynomial.X ^ n).support = {n}
• Polynomial.ofFinsupp_nsmul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : ℕ) (b : AddMonoidAlgebra R ℕ) : { toFinsupp := a • b } = a • { toFinsupp := b }
• Polynomial.toFinsupp_nsmul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : ℕ) (b : Polynomial R) : (a • b).toFinsupp = a • b.toFinsupp
• Polynomial.ofFinsupp_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] {a : AddMonoidAlgebra R ℕ} : { toFinsupp := -a } = -{ toFinsupp := a }
• Polynomial.toFinsupp_C_mul_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a * Polynomial.X).toFinsupp = AddMonoidAlgebra.single 1 a
• Polynomial.toFinsupp_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (a : Polynomial R) : (-a).toFinsupp = -a.toFinsupp
• Polynomial.coeff_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : (Polynomial.C a).coeff n = if n = 0 then a else 0
• Polynomial.support_C_mul_X' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (c : R) : (Polynomial.C c * Polynomial.X).support ⊆ {1}
• Polynomial.sum_add' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f g : ℕ → R → S) : p.sum (f + g) = p.sum f + p.sum g
• Polynomial.C_eq_intCast 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (n : ℤ) : Polynomial.C ↑n = ↑n
• Polynomial.smulCommClass 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] : SMulCommClass S₁ S₂ (Polynomial R)
• Polynomial.isCentralScalar 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [SMulZeroClass Sᵐᵒᵖ R] [IsCentralScalar S R] : IsCentralScalar S (Polynomial R)
• Polynomial.C_inj 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a b : R} [Semiring R] : Polynomial.C a = Polynomial.C b ↔ a = b
• Polynomial.isScalarTower 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R] : IsScalarTower S₁ S₂ (Polynomial R)
• Polynomial.support_C_mul_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {c : R} (h : c ≠ 0) : (Polynomial.C c * Polynomial.X).support = {1}
• Polynomial.smul_sum 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} {T : Type u_2} [AddCommMonoid S] [DistribSMul T S] (p : Polynomial R) (b : T) (f : ℕ → R → S) : b • p.sum f = p.sum fun n a => b • f n a
• Polynomial.sum_C_index 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {a : R} {β : Type u_1} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) : (Polynomial.C a).sum f = f 0 a
• Polynomial.ofFinsupp_zsmul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (a : ℤ) (b : AddMonoidAlgebra R ℕ) : { toFinsupp := a • b } = a • { toFinsupp := b }
• Polynomial.toFinsupp_zsmul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (a : ℤ) (b : Polynomial R) : (a • b).toFinsupp = a • b.toFinsupp
• Polynomial.toFinsupp_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).toFinsupp = AddMonoidAlgebra.single n a
• Polynomial.support_C_mul_X_pow' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
• Polynomial.X_pow_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : Polynomial.X ^ n * p = p * Polynomial.X ^ n
• Polynomial.monomial_injective 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) : Function.Injective ⇑(Polynomial.monomial n)
• Polynomial.ofFinsupp_smul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : AddMonoidAlgebra R ℕ) : { toFinsupp := a • b } = a • { toFinsupp := b }
• Polynomial.toFinsupp_smul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : Polynomial R) : (a • b).toFinsupp = a • b.toFinsupp
• Polynomial.coeff_monomial_same 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : ((Polynomial.monomial n) c).coeff n = c
• 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_sub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] (a b : Polynomial R) : (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
• Polynomial.ofFinsupp_sub 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] {a b : AddMonoidAlgebra R ℕ} : { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
• Polynomial.sum_C_mul_X_pow_eq 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : (p.sum fun n a => Polynomial.C a * Polynomial.X ^ n) = p
• Polynomial.support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) {c : R} (h : c ≠ 0) : (Polynomial.C c * Polynomial.X ^ n).support = {n}
• 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.support_monomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).support ⊆ {n}
• Polynomial.X_mul_C 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (r : R) : Polynomial.X * Polynomial.C r = Polynomial.C r * Polynomial.X
• Polynomial.sum_smul_index 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (b : R) (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) : (b • p).sum f = p.sum fun n a => f n (b * a)
• Polynomial.erase_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {n : ℕ} {a : R} : Polynomial.erase n ((Polynomial.monomial n) a) = 0
• Polynomial.monomial_one_one_eq_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : (Polynomial.monomial 1) 1 = Polynomial.X
• Polynomial.X.eq_1 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial.X = (Polynomial.monomial 1) 1
• Polynomial.C_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {a : R} {n : ℕ} [Semiring R] : Polynomial.C (a ^ n) = Polynomial.C a ^ n
• 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.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.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.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 📋 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

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 6ff4759 serving mathlib revision 76f94b4