Loogle!

Result

Found 115 declarations mentioning Polynomial.support.

• Polynomial.support 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] : Polynomial R → Finset ℕ
• Polynomial.support_X 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] : Polynomial.X.support = {1}
• 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.support_toFinsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : Polynomial R) : p.toFinsupp.coeff.support = p.support
• Polynomial.support_nonempty 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support.Nonempty ↔ p ≠ 0
• Polynomial.support_ofFinsupp 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) : { toFinsupp := p }.support = p.coeff.support
• Polynomial.support_neg 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Ring R] {p : Polynomial R} : (-p).support = p.support
• Polynomial.support_eq_empty 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support = ∅ ↔ p = 0
• 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.card_support_eq_zero 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support.card = 0 ↔ p = 0
• 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.mem_support_iff 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : n ∈ p.support ↔ p.coeff n ≠ 0
• 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.support_X_empty 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (H : 1 = 0) : Polynomial.X.support = ∅
• 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.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.support_X_pow 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (Polynomial.X ^ n).support = {n}
• Polynomial.support_add 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {p q : Polynomial R} : (p + q).support ⊆ p.support ∪ q.support
• Polynomial.support_C_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (a : R) : (Polynomial.C a).support ⊆ {0}
• 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.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_C_mul_X' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (c : R) : (Polynomial.C c * Polynomial.X).support ⊆ {1}
• Polynomial.support_C_mul_X_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (c : R) : (Polynomial.C c * Polynomial.X).support ⊆ {1}
• 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.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.support_monomial 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) {a : R} (h : a ≠ 0) : ((Polynomial.monomial n) a).support = {n}
• 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.support_C_mul_X_pow_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (n : ℕ) (c : R) : (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
• 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.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.support_binomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m : ℕ) (x y : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
• Polynomial.support_binomial_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m : ℕ) (x y : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
• Polynomial.support_trinomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m n : ℕ) (x y z : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆ {k, m, n}
• Polynomial.support_trinomial_subset 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] (k m n : ℕ) (x y z : R) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆ {k, m, n}
• Polynomial.card_support_mul_le 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {p q : Polynomial R} : (p * q).support.card ≤ p.support.card * q.support.card
• Polynomial.support_smul 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} {S : Type v} [Semiring R] [SMulZeroClass S R] (r : S) (p : Polynomial R) : (r • p).support ⊆ p.support
• Polynomial.card_support_binomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2
• Polynomial.support_binomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support = {k, m}
• Polynomial.card_support_trinomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support.card = 3
• Polynomial.support_trinomial 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [Semiring R] {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support = {k, m, n}
• Polynomial.degree_mono 📋 Mathlib.Algebra.Polynomial.Degree.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : Polynomial R} {g : Polynomial S} (h : f.support ⊆ g.support) : f.degree ≤ g.degree
• Polynomial.le_natDegree_of_mem_supp 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → a ≤ p.natDegree
• Polynomial.nonempty_support_iff 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support.Nonempty ↔ p ≠ 0
• Polynomial.card_supp_le_succ_natDegree 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p.support.card ≤ p.natDegree + 1
• Polynomial.supp_subset_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} {m : ℕ} [Semiring R] {p : Polynomial R} (h : p.natDegree < m) : p.support ⊆ Finset.range m
• Polynomial.supp_subset_range_natDegree_succ 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} : p.support ⊆ Finset.range (p.natDegree + 1)
• Polynomial.natDegree_mem_support_of_nonzero 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} (H : p ≠ 0) : p.natDegree ∈ p.support
• Polynomial.le_degree_of_mem_supp 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → ↑a ≤ p.degree
• Polynomial.natDegree_eq_support_max' 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) : p.natDegree = p.support.max' ⋯
• Polynomial.card_support_C_mul_X_pow_le_one 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {c : R} {n : ℕ} : (Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1
• 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.mem_support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] {n a : ℕ} {c : R} (h : a ∈ (Polynomial.C c * Polynomial.X ^ n).support) : a = n
• Polynomial.as_sum_support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.support_map_subset 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : (Polynomial.map f p).support ⊆ p.support
• Polynomial.support_map_of_injective 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) {f : R →+* S} (hf : Function.Injective ⇑f) : (Polynomial.map f p).support = p.support
• 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
• MvPolynomial.support_optionEquivLeft 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] (p : MvPolynomial (Option σ) R) : ((MvPolynomial.optionEquivLeft R σ) p).support = Finset.image (fun m => m none) p.support
• MvPolynomial.nonempty_support_optionEquivLeft 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) {σ : Type u_1} [CommSemiring R] {f : MvPolynomial (Option σ) R} (h : f ≠ 0) : ((MvPolynomial.optionEquivLeft R σ) f).support.Nonempty
• MvPolynomial.nonempty_support_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : ((MvPolynomial.finSuccEquiv R n) f).support.Nonempty
• MvPolynomial.support_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) : ((MvPolynomial.finSuccEquiv R n) f).support = Finset.image (fun m => m 0) f.support
• MvPolynomial.mem_support_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {x : ℕ} : x ∈ ((MvPolynomial.finSuccEquiv R n) f).support ↔ x ∈ (fun m => m 0) '' ↑f.support
• Polynomial.natTrailingDegree_le_of_mem_supp 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (a : ℕ) : a ∈ p.support → p.natTrailingDegree ≤ a
• Polynomial.natTrailingDegree_mem_support_of_nonzero 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} : p ≠ 0 → p.natTrailingDegree ∈ p.support
• Polynomial.natTrailingDegree_eq_support_min' 📋 Mathlib.Algebra.Polynomial.Degree.TrailingDegree
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p ≠ 0) : p.natTrailingDegree = p.support.min' ⋯
• Polynomial.eq_natDegree_of_le_mem_support 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (pn : p.natDegree ≤ n) (ns : n ∈ p.support) : p.natDegree = 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.C_mul_X_pow_eq_self 📋 Mathlib.Algebra.Polynomial.Degree.Monomial
  {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p
• Polynomial.eraseLead_support 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] (f : Polynomial R) : f.eraseLead.support = f.support.erase f.natDegree
• Polynomial.natDegree_notMem_eraseLead_support 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} : f.natDegree ∉ f.eraseLead.support
• Polynomial.ne_natDegree_of_mem_eraseLead_support 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} {a : ℕ} (h : a ∈ f.eraseLead.support) : a ≠ f.natDegree
• Polynomial.lt_natDegree_of_mem_eraseLead_support 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} {a : ℕ} (h : a ∈ f.eraseLead.support) : a < f.natDegree
• Polynomial.eraseLead_natDegree_lt 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 ≤ f.support.card) : f.eraseLead.natDegree < f.natDegree
• Polynomial.card_support_eraseLead 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} : f.eraseLead.support.card = f.support.card - 1
• Polynomial.card_support_eraseLead' 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} {c : ℕ} (fc : f.support.card = c + 1) : f.eraseLead.support.card = c
• Polynomial.card_support_le_one_of_eraseLead_eq_zero 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.eraseLead = 0) : f.support.card ≤ 1
• Polynomial.eraseLead_ne_zero 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 ≤ f.support.card) : f.eraseLead ≠ 0
• Polynomial.eraseLead_support_card_lt 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f ≠ 0) : f.eraseLead.support.card < f.support.card
• Polynomial.card_support_eraseLead_add_one 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f ≠ 0) : f.eraseLead.support.card + 1 = f.support.card
• Polynomial.card_support_eq_one_of_eraseLead_eq_zero 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} (h₀ : f ≠ 0) (h₁ : f.eraseLead = 0) : f.support.card = 1
• Polynomial.card_support_eq_one 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} : f.support.card = 1 ↔ ∃ k x, ∃ (_ : x ≠ 0), f = Polynomial.C x * Polynomial.X ^ k
• Polynomial.card_support_eq' 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {n : ℕ} (k : Fin n → ℕ) (x : Fin n → R) (hk : Function.Injective k) (hx : ∀ (i : Fin n), x i ≠ 0) : (∑ i, Polynomial.C (x i) * Polynomial.X ^ k i).support.card = n
• Polynomial.card_support_eq 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} {n : ℕ} : f.support.card = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, Polynomial.C (x i) * Polynomial.X ^ k i
• Polynomial.card_support_eq_two 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} : f.support.card = 2 ↔ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m
• Polynomial.card_support_eq_three 📋 Mathlib.Algebra.Polynomial.EraseLead
  {R : Type u_1} [Semiring R] {f : Polynomial R} : f.support.card = 3 ↔ ∃ k m n, ∃ (_ : k < m) (_ : m < n), ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n
• Polynomial.reflect_support 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] (N : ℕ) (f : Polynomial R) : (Polynomial.reflect N f).support = Finset.image (⇑(Polynomial.revAt N)) f.support
• Polynomial.reflect_mul_induction 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] (cf cg N O : ℕ) (f g : Polynomial R) (Cf : f.support.card ≤ cf.succ) (Cg : g.support.card ≤ cg.succ) (Nf : f.natDegree ≤ N) (Og : g.natDegree ≤ O) : Polynomial.reflect (N + O) (f * g) = Polynomial.reflect N f * Polynomial.reflect O g
• Polynomial.support_restriction 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Ring R] (p : Polynomial R) : p.restriction.support = p.support
• Polynomial.of_mem_support_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : n ∈ (Polynomial.derivative p).support) : n + 1 ∈ p.support
• Polynomial.mem_support_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] : n ∈ (Polynomial.derivative p).support ↔ n + 1 ∈ p.support
• Polynomial.iterate_derivative_eq_sum 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] p = ∑ x ∈ ((⇑Polynomial.derivative)^[k] p).support, Polynomial.C ((x + k).descFactorial k • p.coeff (x + k)) * Polynomial.X ^ x
• 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
• LaurentPolynomial.support_coeff_toLaurent 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.toLaurent f).coeff.support = Finset.map Nat.castEmbedding f.support
• LaurentPolynomial.toLaurent_support 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.toLaurent f).coeff.support = Finset.map Nat.castEmbedding f.support
• support_subset_support_matPolyEquiv 📋 Mathlib.RingTheory.MatrixPolynomialAlgebra
  {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (m : Matrix n n (Polynomial R)) (i j : n) : (m i j).support ⊆ (matPolyEquiv m).support
• Polynomial.exists_support_eq_of_mem_lifts 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (hlifts : p ∈ Polynomial.lifts f) : ∃ q, Polynomial.map f q = p ∧ q.support = p.support
• Polynomial.support_scaleRoots_le 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) : (p.scaleRoots s).support ⊆ p.support
• Polynomial.support_scaleRoots_eq 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [Semiring R] (p : Polynomial R) {s : R} (hs : s ∈ nonZeroDivisors R) : (p.scaleRoots s).support = p.support
• Polynomial.support_integralNormalization_subset 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} : p.integralNormalization.support ⊆ p.support
• Polynomial.support_integralNormalization 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] [IsCancelMulZero R] {f : Polynomial R} : f.integralNormalization.support = f.support
• Polynomial.support_toSubring 📋 Mathlib.RingTheory.Polynomial.Subring
  {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : (p.toSubring T hp).support = p.support
• IsLocalization.integerNormalization_support 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) : (IsLocalization.integerNormalization M p).support ⊆ p.support
• IsLocalization.scaleRoots_commonDenom_mem_lifts 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_1} [CommRing R] (M : Submonoid R) {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] (p : Polynomial Rₘ) (hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range) : p.scaleRoots ((algebraMap R Rₘ) ↑(IsLocalization.commonDenom M p.support p.coeff)) ∈ Polynomial.lifts (algebraMap R Rₘ)
• mem_reesAlgebra_iff_support 📋 Mathlib.RingTheory.ReesAlgebra
  {R : Type u} [CommRing R] (I : Ideal R) (f : Polynomial R) : f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i
• Polynomial.IsUnitTrinomial.card_support_eq_three 📋 Mathlib.Algebra.Polynomial.UnitTrinomial
  {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) : p.support.card = 3
• Polynomial.IsUnitTrinomial.coeff_isUnit 📋 Mathlib.Algebra.Polynomial.UnitTrinomial
  {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) {k : ℕ} (hk : k ∈ p.support) : IsUnit (p.coeff k)
• Polynomial.isUnitTrinomial_iff 📋 Mathlib.Algebra.Polynomial.UnitTrinomial
  {p : Polynomial ℤ} : p.IsUnitTrinomial ↔ p.support.card = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
• Polynomial.trinomial_support 📋 Mathlib.Algebra.Polynomial.UnitTrinomial
  {R : Type u_1} [Semiring R] {k m n : ℕ} {u v w : R} (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) : (Polynomial.trinomial k m n u v w).support = {k, m, n}
• Polynomial.sum_sq_norm_coeff_eq_circleAverage 📋 Mathlib.Analysis.Polynomial.Fourier
  (p : Polynomial ℂ) : ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ => ‖Polynomial.eval θ p‖ ^ 2) 0 1
• Polynomial.supNorm_def' 📋 Mathlib.Analysis.Polynomial.Norm
  {A : Type u_1} [SeminormedRing A] (p : Polynomial A) : p.supNorm = if hp : p.support.Nonempty then p.support.sup' hp (norm ∘ p.coeff) else 0
• Polynomial.mahlerMeasure_le_sqrt_sum_sq_norm_coeff 📋 Mathlib.Analysis.Polynomial.MahlerMeasure
  (p : Polynomial ℂ) : p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
• Polynomial.hilbertPoly_succ 📋 Mathlib.RingTheory.Polynomial.HilbertPoly
  {F : Type u_1} [Field F] (p : Polynomial F) (d : ℕ) : p.hilbertPoly (d + 1) = ∑ i ∈ p.support, p.coeff i • Polynomial.preHilbertPoly F d i
• Polynomial.support_opRingEquiv 📋 Mathlib.RingTheory.Polynomial.Opposites
  {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) : ((Polynomial.opRingEquiv R) p).support = (MulOpposite.unop p).support

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