Loogle!

Result

Found 262 declarations whose name contains "eval₂". Of these, only the first 200 are shown.

• Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ 📋 Mathlib.Tactic.FieldSimp.Lemmas
  {M : Type u_1} [CommGroupWithZero M] (r₁ r₂ : ℤ) (x : M) {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M} (h : l₁.eval / l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
• Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ 📋 Mathlib.Tactic.FieldSimp.Lemmas
  {M : Type u_1} [CommGroupWithZero M] (r₁ r₂ : ℤ) (x : M) {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M} (h : l₁.eval * l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
• Mathlib.Tactic.Module.NF.add_eq_eval₂ 📋 Mathlib.Tactic.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (r₁ r₂ : R) (x : M) {l₁ l₂ l : Mathlib.Tactic.Module.NF R M} (h : l₁.eval + l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
• Mathlib.Tactic.Module.NF.sub_eq_eval₂ 📋 Mathlib.Tactic.Module
  {R : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r₁ r₂ : R) (x : M) {l₁ l₂ l : Mathlib.Tactic.Module.NF R M} (h : l₁.eval - l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
• Polynomial.eval₂ 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) : S
• Polynomial.eval₂_id 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval₂ (RingHom.id R) x p = Polynomial.eval x p
• Polynomial.eval₂_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x Polynomial.X = x
• Polynomial.eval₂RingHom 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) : Polynomial R →+* S
• Polynomial.eval₂_eq_eval_map 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) {x : S} : Polynomial.eval₂ f x p = Polynomial.eval x (Polynomial.map f p)
• Polynomial.eval₂_natCast 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (n : ℕ) : Polynomial.eval₂ f x ↑n = ↑n
• Polynomial.eval₂_zero 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x 0 = 0
• Polynomial.eval₂_one 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x 1 = 1
• Polynomial.eval₂_multiset_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (s : Multiset (Polynomial R)) (x : S) : Polynomial.eval₂ f x s.sum = (Multiset.map (Polynomial.eval₂ f x) s).sum
• Polynomial.eval₂_ofNat 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) : Polynomial.eval₂ f a (OfNat.ofNat n) = OfNat.ofNat n
• Polynomial.eval₂AddMonoidHom 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial R →+ S
• Polynomial.eval₂RingHom_comp_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) : (Polynomial.eval₂RingHom f x).comp Polynomial.C = f
• Polynomial.eval₂RingHom' 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) : Polynomial R →+* S
• Polynomial.eval₂_finsetSum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {ι : Type y} [Semiring R] [Semiring S] (f : R →+* S) (s : Finset ι) (g : ι → Polynomial R) (x : S) : Polynomial.eval₂ f x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval₂ f x (g i)
• Polynomial.eval₂_finset_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {ι : Type y} [Semiring R] [Semiring S] (f : R →+* S) (s : Finset ι) (g : ι → Polynomial R) (x : S) : Polynomial.eval₂ f x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval₂ f x (g i)
• Polynomial.eval₂_list_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (l : List (Polynomial R)) (x : S) : Polynomial.eval₂ f x l.sum = (List.map (Polynomial.eval₂ f x) l).sum
• Polynomial.eval₂_X_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (Polynomial.X * p) = Polynomial.eval₂ f x p * x
• Polynomial.eval₂_mul_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (p * Polynomial.X) = Polynomial.eval₂ f x p * x
• Polynomial.eval₂_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] (f : R →+* S) [Semiring T] (p : Polynomial T) (g : ℕ → T → Polynomial R) (x : S) : Polynomial.eval₂ f x (p.sum g) = p.sum fun n a => Polynomial.eval₂ f x (g n a)
• Polynomial.eval₂_congr 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f g : R →+* S} {s t : S} {φ ψ : Polynomial R} : f = g → s = t → φ = ψ → Polynomial.eval₂ f s φ = Polynomial.eval₂ g t ψ
• Polynomial.eval₂_X_pow 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) {n : ℕ} : Polynomial.eval₂ f x (Polynomial.X ^ n) = x ^ n
• Polynomial.eval₂_neg 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) {x : S} : Polynomial.eval₂ f x (-p) = -Polynomial.eval₂ f x p
• Polynomial.eval₂_add 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (p + q) = Polynomial.eval₂ f x p + Polynomial.eval₂ f x q
• Polynomial.eval₂_at_natCast 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ℕ) : Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)
• Polynomial.eval₂_list_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (l : List (Polynomial R)) (x : S) : Polynomial.eval₂ f x l.prod = (List.map (Polynomial.eval₂ f x) l).prod
• Polynomial.eval₂_multiset_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Multiset (Polynomial R)) (x : S) : Polynomial.eval₂ f x s.prod = (Multiset.map (Polynomial.eval₂ f x) s).prod
• Polynomial.eval₂_at_apply 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (r : R) : Polynomial.eval₂ f (f r) p = f (Polynomial.eval r p)
• Polynomial.coe_eval₂RingHom 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] (f : R →+* S) (x : S) : ⇑(Polynomial.eval₂RingHom f x) = Polynomial.eval₂ f x
• Polynomial.eval₂_at_one 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) : Polynomial.eval₂ f 1 p = f (Polynomial.eval 1 p)
• Polynomial.eval₂_dvd 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) : p ∣ q → Polynomial.eval₂ f x p ∣ Polynomial.eval₂ f x q
• Polynomial.eval₂_finsetProd 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {ι : Type y} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Finset ι) (g : ι → Polynomial R) (x : S) : Polynomial.eval₂ f x (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.eval₂ f x (g i)
• Polynomial.eval₂_finset_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {ι : Type y} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Finset ι) (g : ι → Polynomial R) (x : S) : Polynomial.eval₂ f x (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.eval₂ f x (g i)
• Polynomial.eval₂_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
• Polynomial.eval₂_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {a : R} [Semiring R] [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x (Polynomial.C a) = f a
• Polynomial.eval₂_at_ofNat 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] : Polynomial.eval₂ f (OfNat.ofNat n) p = f (Polynomial.eval (OfNat.ofNat n) p)
• Polynomial.eval₂_def 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) : Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
• Polynomial.eval₂_eq_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} {x : S} : Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
• Polynomial.eval₂_mul_eq_zero_of_left 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (q : Polynomial R) (hp : Polynomial.eval₂ f x p = 0) : Polynomial.eval₂ f x (p * q) = 0
• Polynomial.eval₂_mul_eq_zero_of_right 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (p : Polynomial R) (hq : Polynomial.eval₂ f x q = 0) : Polynomial.eval₂ f x (p * q) = 0
• Polynomial.eval₂_pow 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (n : ℕ) : Polynomial.eval₂ f x (p ^ n) = Polynomial.eval₂ f x p ^ n
• Polynomial.eval₂_at_intCast 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) (n : ℤ) : Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)
• Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (x : S) (h : p ∣ q) (h0 : Polynomial.eval₂ f x p = 0) : Polynomial.eval₂ f x q = 0
• Polynomial.eval₂RingHom'_apply 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) (p : Polynomial R) : (Polynomial.eval₂RingHom' f x hf) p = Polynomial.eval₂ f x p
• Polynomial.eval₂_sub 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) {x : S} : Polynomial.eval₂ f x (p - q) = Polynomial.eval₂ f x p - Polynomial.eval₂ f x q
• Polynomial.eval₂_mul_noncomm 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x) : Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
• Polynomial.eval₂_list_prod_noncomm 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (ps : List (Polynomial R)) (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) : Polynomial.eval₂ f x ps.prod = (List.map (Polynomial.eval₂ f x) ps).prod
• Polynomial.eval₂AddMonoidHom_apply 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : Polynomial R) : (Polynomial.eval₂AddMonoidHom f x) p = Polynomial.eval₂ f x p
• 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.eval₂_mul_C' 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {a : R} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) (h : Commute (f a) x) : Polynomial.eval₂ f x (p * Polynomial.C a) = Polynomial.eval₂ f x p * f a
• Polynomial.eval₂_ofFinsupp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {x : S} {p : AddMonoidAlgebra R ℕ} : Polynomial.eval₂ f x { toFinsupp := p } = (AddMonoidAlgebra.liftNC ↑f ⇑((powersHom S) x)) p
• Polynomial.eval₂_comp' 📋 Mathlib.Algebra.Polynomial.Eval.Algebra
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p q : Polynomial R) : Polynomial.eval₂ (algebraMap R S) x (p.comp q) = Polynomial.eval₂ (algebraMap R S) (Polynomial.eval₂ (algebraMap R S) x q) p
• Polynomial.eval₂_mul' 📋 Mathlib.Algebra.Polynomial.Eval.Algebra
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p q : Polynomial R) : Polynomial.eval₂ (algebraMap R S) x (p * q) = Polynomial.eval₂ (algebraMap R S) x p * Polynomial.eval₂ (algebraMap R S) x q
• Polynomial.eval₂_pow' 📋 Mathlib.Algebra.Polynomial.Eval.Algebra
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) (n : ℕ) : Polynomial.eval₂ (algebraMap R S) x (p ^ n) = Polynomial.eval₂ (algebraMap R S) x p ^ n
• Polynomial.eval₂_C_X 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.eval₂ Polynomial.C Polynomial.X p = p
• Polynomial.eval₂_at_zero 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) : Polynomial.eval₂ f 0 p = f (p.coeff 0)
• Polynomial.eval₂_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} {T : Type w} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) [Semiring T] (g : S →+* T) (x : T) : Polynomial.eval₂ g x (Polynomial.map f p) = Polynomial.eval₂ (g.comp f) x p
• Polynomial.eval₂_hom 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : R) : Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)
• Polynomial.hom_eval₂ 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} {T : Type w} [Semiring R] (p : Polynomial R) [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) (x : S) : g (Polynomial.eval₂ f x p) = Polynomial.eval₂ (g.comp f) (g x) p
• Polynomial.eval₂_comp 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) {x : S} : Polynomial.eval₂ f x (p.comp q) = Polynomial.eval₂ f (Polynomial.eval₂ f x q) p
• Polynomial.iterate_comp_eval₂ 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (k : ℕ) (t : S) : Polynomial.eval₂ f t (p.comp^[k] q) = (fun x => Polynomial.eval₂ f x p)^[k] (Polynomial.eval₂ f t q)
• Polynomial.eval₂_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
• Polynomial.eval₂_eq_sum_range 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
• Polynomial.eval₂AlgHom 📋 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) (b : B) (hf : ∀ (a : A), Commute (f a) b) : Polynomial A →ₐ[R] B
• Polynomial.isRoot_of_eval₂_map_eq_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {r : R} : Polynomial.eval₂ f (f r) p = 0 → p.IsRoot r
• Polynomial.algHom_eval₂_algebraMap 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (p : Polynomial R) (f : A →ₐ[R] B) (a : A) : f (Polynomial.eval₂ (algebraMap R A) a p) = Polynomial.eval₂ (algebraMap R B) (f a) p
• Polynomial.ringHom_eval₂_intCastRingHom 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} {S : Type u_4} [Ring R] [Ring S] (p : Polynomial ℤ) (f : R →+* S) (r : R) : f (Polynomial.eval₂ (Int.castRingHom R) r p) = Polynomial.eval₂ (Int.castRingHom S) (f r) p
• Polynomial.eval₂_intCastRingHom_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [Ring R] (p : Polynomial ℤ) (f : Polynomial ℤ →+* R) : Polynomial.eval₂ (Int.castRingHom R) (f Polynomial.X) p = f p
• Polynomial.eval₂AlgHom_apply 📋 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) (b : B) (hf : ∀ (a : A), Commute (f a) b) (p : Polynomial A) : (Polynomial.eval₂AlgHom f b hf) p = Polynomial.eval₂ (↑f) b p
• Polynomial.eval₂_algebraMap_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (f : Polynomial R →ₐ[R] A) : Polynomial.eval₂ (algebraMap R A) (f Polynomial.X) p = f p
• Polynomial.mapAlgHom_eq_eval₂AlgHom_CAlgHom 📋 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) : Polynomial.mapAlgHom f = Polynomial.eval₂AlgHom (Polynomial.CAlgHom.comp f) Polynomial.X ⋯
• MvPolynomial.eval₂ 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : S₁
• MvPolynomial.eval₂_X 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : σ) : MvPolynomial.eval₂ f g (MvPolynomial.X n) = g n
• MvPolynomial.eval₂_eta 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X p = p
• MvPolynomial.eval₂Hom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial σ R →+* S₁
• MvPolynomial.eval₂AlgHom 📋 Mathlib.Algebra.MvPolynomial.Eval
  (R : Type u) {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σ → S₁) : MvPolynomial σ R →ₐ[R] S₁
• MvPolynomial.eval₂_one 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g 1 = 1
• MvPolynomial.eval₂_zero 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g 0 = 0
• MvPolynomial.eval₂_sum 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R) : MvPolynomial.eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, MvPolynomial.eval₂ f g (p x)
• MvPolynomial.eval₂_natCast 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : ℕ) : MvPolynomial.eval₂ f g ↑n = ↑n
• MvPolynomial.eval₂_prod 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R) : MvPolynomial.eval₂ f g (∏ x ∈ s, p x) = ∏ x ∈ s, MvPolynomial.eval₂ f g (p x)
• MvPolynomial.eval₂_assoc 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R) : MvPolynomial.eval₂ f (fun t => MvPolynomial.eval₂ f g (q t)) p = MvPolynomial.eval₂ f g (MvPolynomial.eval₂ MvPolynomial.C q p)
• MvPolynomial.eval₂_congr 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g₁ g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → MvPolynomial.coeff c p ≠ 0 → g₁ i = g₂ i) : MvPolynomial.eval₂ f g₁ p = MvPolynomial.eval₂ f g₂ p
• MvPolynomial.eval₂_id 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {σ : Type u_1} [CommSemiring R] {g : σ → R} (p : MvPolynomial σ R) : MvPolynomial.eval₂ (RingHom.id R) g p = (MvPolynomial.eval g) p
• MvPolynomial.eval₂_ofNat 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : ℕ) [n.AtLeastTwo] : MvPolynomial.eval₂ f g (OfNat.ofNat n) = OfNat.ofNat n
• MvPolynomial.eval₂_X_pow 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) {s : σ} {n : ℕ} : MvPolynomial.eval₂ f g (MvPolynomial.X s ^ n) = g s ^ n
• MvPolynomial.eval₂_dvd 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) {p q : MvPolynomial σ R} (h : p ∣ q) : MvPolynomial.eval₂ f g p ∣ MvPolynomial.eval₂ f g q
• MvPolynomial.eval₂Hom_X' 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (i : σ) : (MvPolynomial.eval₂Hom f g) (MvPolynomial.X i) = g i
• MvPolynomial.eval₂Hom_zero' 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) : (MvPolynomial.eval₂Hom f fun x => 0) = f.comp MvPolynomial.constantCoeff
• MvPolynomial.eval₂_mul 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R} : MvPolynomial.eval₂ f g (p * q) = MvPolynomial.eval₂ f g p * MvPolynomial.eval₂ f g q
• MvPolynomial.coe_eval₂Hom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : ⇑(MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂ f g
• MvPolynomial.eval₂_pow 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R} {n : ℕ} : MvPolynomial.eval₂ f g (p ^ n) = MvPolynomial.eval₂ f g p ^ n
• MvPolynomial.eval₂_mul_eq_zero_of_left 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) (hp : MvPolynomial.eval₂ f g p = 0) : MvPolynomial.eval₂ f g (p * q) = 0
• MvPolynomial.eval₂_mul_eq_zero_of_right 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) (hq : MvPolynomial.eval₂ f g q = 0) : MvPolynomial.eval₂ f g (p * q) = 0
• MvPolynomial.eval₂Hom_zero 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) : MvPolynomial.eval₂Hom f 0 = f.comp MvPolynomial.constantCoeff
• MvPolynomial.eval₂_add 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g (p + q) = MvPolynomial.eval₂ f g p + MvPolynomial.eval₂ f g q
• MvPolynomial.eval₂_C 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (a : R) : MvPolynomial.eval₂ f g (MvPolynomial.C a) = f a
• MvPolynomial.map_eq_eval₂Hom_C_comp 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) : MvPolynomial.map f = MvPolynomial.eval₂Hom (MvPolynomial.C.comp f) MvPolynomial.X
• MvPolynomial.eval₂AlgHom_X 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σ → S₁) (i : σ) : (MvPolynomial.eval₂AlgHom R g) (MvPolynomial.X i) = g i
• MvPolynomial.eval₂_comp_left 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (k.comp f) (⇑k ∘ g) p
• MvPolynomial.coe_eval₂AlgHom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σ → S₁) : ⇑(MvPolynomial.eval₂AlgHom R g) = MvPolynomial.eval₂ (algebraMap R S₁) g
• MvPolynomial.eval₂_zero'_apply 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f (fun x => 0) p = f (MvPolynomial.constantCoeff p)
• MvPolynomial.eval₂_zero_apply 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f 0 p = f (MvPolynomial.constantCoeff p)
• MvPolynomial.eval₂_eq' 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) : MvPolynomial.eval₂ g X f = ∑ d ∈ f.support, g (MvPolynomial.coeff d f) * ∏ i, X i ^ d i
• MvPolynomial.eval₂_mem 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {f : R →+* S} {p : MvPolynomial σ R} {s : subS} (hs : ∀ i ∈ p.support, f (MvPolynomial.coeff i p) ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) : MvPolynomial.eval₂ f v p ∈ s
• MvPolynomial.eval₂_eq 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) : MvPolynomial.eval₂ g X f = ∑ d ∈ f.support, g (MvPolynomial.coeff d f) * ∏ i ∈ d.support, X i ^ d i
• MvPolynomial.comp_eval₂Hom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) : φ.comp (MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂Hom (φ.comp f) fun i => φ (g i)
• MvPolynomial.eval₂_comp 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → R) (p : MvPolynomial σ R) : f ((MvPolynomial.eval g) p) = MvPolynomial.eval₂ f (⇑f ∘ g) p
• MvPolynomial.eval₂Hom_eq_zero 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (g : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0) : (MvPolynomial.eval₂Hom f g) φ = 0
• MvPolynomial.eval₂_map 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) : MvPolynomial.eval₂ φ g ((MvPolynomial.map f) p) = MvPolynomial.eval₂ (φ.comp f) g p
• MvPolynomial.eval₂_mul_C 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g (p * MvPolynomial.C a) = MvPolynomial.eval₂ f g p * f a
• MvPolynomial.eval₂Hom_C 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (r : R) : (MvPolynomial.eval₂Hom f g) (MvPolynomial.C r) = f r
• MvPolynomial.eval₂Hom_zero'_apply 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f fun x => 0) p = f (MvPolynomial.constantCoeff p)
• MvPolynomial.eval₂_eq_eval_map 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f g p = (MvPolynomial.eval g) ((MvPolynomial.map f) p)
• MvPolynomial.aeval_eq_eval₂Hom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (p : MvPolynomial σ R) : (MvPolynomial.aeval f) p = (MvPolynomial.eval₂Hom (algebraMap R S₁) f) p
• MvPolynomial.eval₂AlgHom_apply 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σ → S₁) (P : MvPolynomial σ R) : (MvPolynomial.eval₂AlgHom R g) P = (MvPolynomial.eval₂Hom (algebraMap R S₁) g) P
• MvPolynomial.eval₂Hom_zero_apply 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f 0) p = f (MvPolynomial.constantCoeff p)
• MvPolynomial.eval₂Hom_congr 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f₁ f₂ : R →+* S₁} {g₁ g₂ : σ → S₁} {p₁ p₂ : MvPolynomial σ R} : f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
• MvPolynomial.eval₂_comp_right 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ k (⇑k ∘ g) ((MvPolynomial.map f) p)
• MvPolynomial.eval₂_map_comp_C 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {ι : Type u_2} (f : R →+* S₁) (h : ι → MvPolynomial σ S₁) (p : MvPolynomial ι R) : MvPolynomial.eval₂ ((MvPolynomial.map f).comp MvPolynomial.C) h p = MvPolynomial.eval₂ MvPolynomial.C h ((MvPolynomial.map f) p)
• MvPolynomial.eval₂_monomial 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g ((MvPolynomial.monomial s) a) = f a * s.prod fun n e => g n ^ e
• MvPolynomial.eval_eval₂ 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {τ : Type u_3} {x : τ → S} [CommSemiring S] (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (p : MvPolynomial σ R) : (MvPolynomial.eval x) (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ ((MvPolynomial.eval x).comp f) (fun s => (MvPolynomial.eval x) (g s)) p
• MvPolynomial.map_eval₂Hom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) : φ ((MvPolynomial.eval₂Hom f g) p) = (MvPolynomial.eval₂Hom (φ.comp f) fun i => φ (g i)) p
• MvPolynomial.eval₂Hom_smul 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (r : R) (P : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f g) (r • P) = f r • (MvPolynomial.eval₂Hom f g) P
• MvPolynomial.eval₂_mul_monomial 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {s : σ →₀ ℕ} {a : R} : MvPolynomial.eval₂ f g (p * (MvPolynomial.monomial s) a) = MvPolynomial.eval₂ f g p * f a * s.prod fun n e => g n ^ e
• MvPolynomial.eval₂Hom_monomial 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.monomial d) r) = f r * d.prod fun i k => g i ^ k
• MvPolynomial.eval₂Hom_map_hom 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom φ g) ((MvPolynomial.map f) p) = (MvPolynomial.eval₂Hom (φ.comp f) g) p
• MvPolynomial.map_eval₂ 📋 Mathlib.Algebra.MvPolynomial.Eval
  {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R) : (MvPolynomial.map f) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.map f) ∘ g) ((MvPolynomial.map f) p)
• MvPolynomial.eval₂_cast_comp 📋 Mathlib.Algebra.MvPolynomial.Rename
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) : MvPolynomial.eval₂ c (g ∘ f) p = MvPolynomial.eval₂ c g ((MvPolynomial.rename f) p)
• MvPolynomial.eval₂_rename 📋 Mathlib.Algebra.MvPolynomial.Rename
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f g ((MvPolynomial.rename k) p) = MvPolynomial.eval₂ f (g ∘ k) p
• MvPolynomial.eval₂_rename_prod_mk 📋 Mathlib.Algebra.MvPolynomial.Rename
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) : MvPolynomial.eval₂ f g ((MvPolynomial.rename (Prod.mk i)) p) = MvPolynomial.eval₂ f (fun j => g (i, j)) p
• MvPolynomial.eval₂Hom_rename 📋 Mathlib.Algebra.MvPolynomial.Rename
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.rename k) p) = (MvPolynomial.eval₂Hom f (g ∘ k)) p
• MvPolynomial.rename_prod_mk_eval₂ 📋 Mathlib.Algebra.MvPolynomial.Rename
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) (j : τ) (g : σ → MvPolynomial σ R) : (MvPolynomial.rename (Prod.mk j)) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (fun x => (MvPolynomial.rename (Prod.mk j)) (g x)) p
• MvPolynomial.rename_eval₂ 📋 Mathlib.Algebra.MvPolynomial.Rename
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (k : σ → τ) (p : MvPolynomial σ R) (g : τ → MvPolynomial σ R) : (MvPolynomial.rename k) (MvPolynomial.eval₂ MvPolynomial.C (g ∘ k) p) = MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.rename k) ∘ g) ((MvPolynomial.rename k) p)
• MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars 📋 Mathlib.Algebra.MvPolynomial.Variables
  {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] (f : R →+* S) {g : σ → S} {p : MvPolynomial σ R} (hp : ∀ i ∈ p.vars, g i = 0) : (MvPolynomial.eval₂Hom f g) p = f (MvPolynomial.constantCoeff p)
• MvPolynomial.eval₂Hom_congr' 📋 Mathlib.Algebra.MvPolynomial.Variables
  {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] {f₁ f₂ : R →+* S} {g₁ g₂ : σ → S} {p₁ p₂ : MvPolynomial σ R} : f₁ = f₂ → (∀ i ∈ p₁.vars, i ∈ p₂.vars → g₁ i = g₂ i) → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
• MvPolynomial.eval₂_neg 📋 Mathlib.Algebra.MvPolynomial.CommRing
  {R : Type u} {S : Type v} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) [CommRing S] (f : R →+* S) (g : σ → S) : MvPolynomial.eval₂ f g (-p) = -MvPolynomial.eval₂ f g p
• MvPolynomial.eval₂_sub 📋 Mathlib.Algebra.MvPolynomial.CommRing
  {R : Type u} {S : Type v} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} [CommRing S] (f : R →+* S) (g : σ → S) : MvPolynomial.eval₂ f g (p - q) = MvPolynomial.eval₂ f g p - MvPolynomial.eval₂ f g q
• MvPolynomial.eval₂Hom_X 📋 Mathlib.Algebra.MvPolynomial.CommRing
  {S : Type v} [CommRing S] {R : Type u} (c : ℤ →+* S) (f : MvPolynomial R ℤ →+* S) (x : MvPolynomial R ℤ) : MvPolynomial.eval₂ c (⇑f ∘ MvPolynomial.X) x = f x
• Polynomial.natDegree_pos_of_eval₂_root 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : 0 < p.natDegree
• Polynomial.degree_pos_of_eval₂_root 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p ≠ 0) (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : 0 < p.degree
• MvPolynomial.eval₂_const_pUnitAlgEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : MvPolynomial PUnit.{u_4 + 1} R} {φ : R →+* S} {a : S} : Polynomial.eval₂ φ a ((MvPolynomial.pUnitAlgEquiv R) f) = MvPolynomial.eval₂ φ (fun x => a) f
• MvPolynomial.eval₂_pUnitAlgEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : MvPolynomial PUnit.{u_4 + 1} R} {φ : R →+* S} {a : PUnit.{u_4 + 1} → S} : Polynomial.eval₂ φ (a default) ((MvPolynomial.pUnitAlgEquiv R) f) = MvPolynomial.eval₂ φ a f
• MvPolynomial.eval₂_const_uniqueAlgEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] [Unique σ] {f : MvPolynomial σ R} {φ : R →+* S} {a : S} : Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R σ) f) = MvPolynomial.eval₂ φ (fun x => a) f
• MvPolynomial.eval₂_uniqueAlgEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] [Unique σ] {f : MvPolynomial σ R} {φ : R →+* S} {a : σ → S} : Polynomial.eval₂ φ (a default) ((MvPolynomial.uniqueAlgEquiv R σ) f) = MvPolynomial.eval₂ φ a f
• MvPolynomial.eval₂_const_pUnitAlgEquiv_symm 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : Polynomial R} {φ : R →+* S} {a : S} : MvPolynomial.eval₂ φ (fun x => a) ((MvPolynomial.pUnitAlgEquiv R).symm f) = Polynomial.eval₂ φ a f
• MvPolynomial.eval₂_pUnitAlgEquiv_symm 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {f : Polynomial R} {φ : R →+* S} {a : Unit → S} : MvPolynomial.eval₂ φ a ((MvPolynomial.pUnitAlgEquiv R).symm f) = Polynomial.eval₂ φ (a ()) f
• MvPolynomial.eval₂_const_uniqueAlgEquiv_symm 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] [Unique σ] {f : Polynomial R} {φ : R →+* S} {a : S} : MvPolynomial.eval₂ φ (fun x => a) ((MvPolynomial.uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ a f
• MvPolynomial.eval₂_uniqueAlgEquiv_symm 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] [Unique σ] {f : Polynomial R} {φ : R →+* S} {a : σ → S} : MvPolynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ (a default) f
• Polynomial.eval₂_reverse_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (f : Polynomial R) : Polynomial.eval₂ i (⅟x) f.reverse = 0 ↔ Polynomial.eval₂ i x f = 0
• Polynomial.eval₂_reverse_mul_pow 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (f : Polynomial R) : Polynomial.eval₂ i (⅟x) f.reverse * x ^ f.natDegree = Polynomial.eval₂ i x f
• Polynomial.eval₂_reflect_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : Polynomial R) (hf : f.natDegree ≤ N) : Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) = 0 ↔ Polynomial.eval₂ i x f = 0
• Polynomial.eval₂_reflect_mul_pow 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : Polynomial R) (hf : f.natDegree ≤ N) : Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) * x ^ N = Polynomial.eval₂ i x f
• MvPolynomial.map_mvPolynomial_eq_eval₂ 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {σ : Type v} [CommRing R] {S : Type u_2} [CommSemiring S] [Finite σ] (ϕ : MvPolynomial σ R →+* S) (p : MvPolynomial σ R) : ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p
• Polynomial.eval₂_restriction 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {S : Type u_1} [Ring R] [Semiring S] {f : R →+* S} {x : S} {p : Polynomial R} : Polynomial.eval₂ f x p = Polynomial.eval₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction
• Polynomial.derivative_eval₂_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p q : Polynomial R) : Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) = Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q
• Polynomial.eval₂_modByMonic_eq_self_of_root 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {p q : Polynomial R} {x : S} (hx : Polynomial.eval₂ f x q = 0) : Polynomial.eval₂ f x (p %ₘ q) = Polynomial.eval₂ f x p
• Polynomial.eval₂_smul 📋 Mathlib.Algebra.Polynomial.Eval.SMul
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (g : R →+* S) (p : Polynomial R) (x : S) {s : R} : Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p
• Polynomial.eval₂_gcd_eq_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : Polynomial R} {α : k} (hf : Polynomial.eval₂ ϕ α f = 0) (hg : Polynomial.eval₂ ϕ α g = 0) : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
• Polynomial.eval₂_primPart_eq_zero 📋 Mathlib.RingTheory.Polynomial.Content
  {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {S : Type u_2} [CommSemiring S] [IsDomain S] {f : R →+* S} (hinj : Function.Injective ⇑f) {p : Polynomial R} {s : S} (hpzero : p ≠ 0) (hp : Polynomial.eval₂ f s p = 0) : Polynomial.eval₂ f s p.primPart = 0
• UniformOnFun.continuousAt_eval₂ 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] {f : UniformOnFun α β 𝔖} {x : α} (h𝔖 : ∃ V ∈ 𝔖, V ∈ nhds x) (hc : ContinuousAt ((UniformOnFun.toFun 𝔖) f) x) : ContinuousAt (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) (f, x)
• UniformOnFun.continuousOn_eval₂ 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h𝔖 : ∀ (x : α), ∃ V ∈ 𝔖, V ∈ nhds x) : ContinuousOn (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) {fx | ContinuousAt ((UniformOnFun.toFun 𝔖) fx.1) fx.2}
• LaurentPolynomial.eval₂ 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) : LaurentPolynomial R →+* S
• LaurentPolynomial.eval₂_T_n 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (n : ℕ) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.T ↑n) = ↑x ^ n
• LaurentPolynomial.eval₂_T_neg_n 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (n : ℕ) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.T (-↑n)) = ↑x⁻¹ ^ n
• LaurentPolynomial.eval₂_T 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (n : ℤ) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.T n) = ↑(x ^ n)
• LaurentPolynomial.eval₂_C 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r) = f r
• LaurentPolynomial.eval₂_toLaurent 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (p : Polynomial R) : (LaurentPolynomial.eval₂ f x) (Polynomial.toLaurent p) = Polynomial.eval₂ f (↑x) p
• LaurentPolynomial.eval₂_C_mul_T_n 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R) (n : ℕ) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r * LaurentPolynomial.T ↑n) = f r * ↑x ^ n
• LaurentPolynomial.eval₂_C_mul_T_neg_n 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R) (n : ℕ) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r * LaurentPolynomial.T (-↑n)) = f r * ↑x⁻¹ ^ n
• LaurentPolynomial.eval₂_C_mul_T 📋 Mathlib.Algebra.Polynomial.Laurent
  {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R) (n : ℤ) : (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r * LaurentPolynomial.T n) = f r * ↑(x ^ n)
• Matrix.mvPolynomialX_map_eval₂ 📋 Mathlib.LinearAlgebra.Matrix.MvPolynomial
  {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (A : Matrix m n S) : (Matrix.mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun p => A p.1 p.2) = A
• Polynomial.eval₂_derivative_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : Polynomial.eval x (Polynomial.derivative f) = f.leadingCoeff * (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum
• Polynomial.scaleRoots_eval₂_eq_zero 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} {S : Type u_2} [Semiring S] [CommSemiring R] {p : Polynomial S} (f : S →+* R) {r : R} {s : S} (hr : Polynomial.eval₂ f r p = 0) : Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = 0
• Polynomial.scaleRoots_eval₂_mul 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} {S : Type u_2} [Semiring S] [CommSemiring R] {p : Polynomial S} (f : S →+* R) (r : R) (s : S) : Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = f s ^ p.natDegree * Polynomial.eval₂ f r p
• Polynomial.scaleRoots_eval₂_mul_of_commute 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {S : Type u_2} {A : Type u_3} [Semiring S] [Semiring A] {p : Polynomial S} (f : S →+* A) (a : A) (s : S) (hsa : Commute (f s) a) (hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)) : Polynomial.eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * Polynomial.eval₂ f a p
• Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {S : Type u_2} {K : Type u_4} [Semiring S] [Field K] {p : Polynomial S} {f : S →+* K} (hf : Function.Injective ⇑f) {r s : S} (hr : Polynomial.eval₂ f (f r / f s) p = 0) (hs : s ∈ nonZeroDivisors S) : Polynomial.eval₂ f (f r) (p.scaleRoots s) = 0
• Polynomial.integralNormalization_eval₂_eq_zero 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] {p : Polynomial R} (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) : Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
• Polynomial.integralNormalization_eval₂_leadingCoeff_mul 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) : Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
• Polynomial.integralNormalization_eval₂_eq_zero_of_commute 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {A : Type u_1} [Semiring A] {p : Polynomial R} (f : R →+* A) {z : A} (hz : Polynomial.eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r' : R}, Commute (f r) (f r')) (inj : ∀ (x : R), f x = 0 → x = 0) : Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
• Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {p : Polynomial R} {A : Type u_1} [Semiring A] (h : 1 ≤ p.natDegree) (f : R →+* A) (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r' : R}, Commute (f r) (f r')) : Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
• IsLocalization.integerNormalization_eval₂_eq_zero 📋 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] {R' : Type u_3} [CommRing R'] (g : S →+* R') (p : Polynomial S) {x : R'} (hx : Polynomial.eval₂ g x p = 0) : Polynomial.eval₂ (g.comp (algebraMap R S)) x (IsLocalization.integerNormalization M p) = 0
• Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} {A : Type u_1} [CommRing R] [CommRing A] {f : R →+* A} (hf : Function.Injective ⇑f) {p : Polynomial R} (hp : p.Monic) (x y : R) (z : A) (h : Polynomial.eval₂ f z p = 0) (hz : f x * z = f y) : x ∣ y ^ p.natDegree
• Ideal.eval₂_C_mk_eq_zero 📋 Mathlib.RingTheory.Polynomial.Quotient
  {R : Type u_1} [CommRing R] {I : Ideal R} (f : Polynomial R) : f ∈ Ideal.map Polynomial.C I → (Polynomial.eval₂RingHom (Polynomial.C.comp (Ideal.Quotient.mk I)) Polynomial.X) f = 0
• MvPolynomial.eval₂_C_mk_eq_zero 📋 Mathlib.RingTheory.Polynomial.Quotient
  {R : Type u_1} {σ : Type u_2} [CommRing R] {I : Ideal R} {a : MvPolynomial σ R} (ha : a ∈ Ideal.map MvPolynomial.C I) : (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0
• AdjoinRoot.eval₂_root 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} [CommRing R] (f : Polynomial R) : Polynomial.eval₂ (AdjoinRoot.of f) (AdjoinRoot.root f) f = 0
• Polynomial.Separable.eval₂_derivative_ne_zero 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] [Nontrivial S] (f : R →+* S) {p : Polynomial R} (h : p.Separable) {x : S} (hx : Polynomial.eval₂ f x p = 0) : Polynomial.eval₂ f x (Polynomial.derivative p) ≠ 0
• FixedPoints.minpoly.eval₂' 📋 Mathlib.FieldTheory.Fixed
  (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
• FixedPoints.minpoly.eval₂ 📋 Mathlib.FieldTheory.Fixed
  (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
• FixedPoints.minpoly.of_eval₂ 📋 Mathlib.FieldTheory.Fixed
  (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) (f : Polynomial ↥(FixedPoints.subfield G F)) (hf : Polynomial.eval₂ (FixedPoints.subfield G F).subtype x f = 0) : FixedPoints.minpoly G F x ∣ f
• IsAlgClosed.exists_eval₂_eq_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] {R : Type u_1} [Ring R] [IsSimpleRing R] [IsAlgClosed k] (f : R →+* k) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ x, Polynomial.eval₂ f x p = 0
• IsAlgClosed.exists_eval₂_eq_zero_of_injective 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] {R : Type u_1} [Semiring R] [IsAlgClosed k] (f : R →+* k) (hf : Function.Injective ⇑f) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ x, Polynomial.eval₂ f x p = 0
• ascPochhammer_eval₂ 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  {S : Type u} [Semiring S] {T : Type v} [Semiring T] (f : S →+* T) (n : ℕ) (t : T) : Polynomial.eval t (ascPochhammer T n) = Polynomial.eval₂ f t (ascPochhammer S n)
• MvPolynomial.eval₂Hom_comp_C 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ → S) : (MvPolynomial.eval₂Hom f g).comp MvPolynomial.C = f
• MvPolynomial.eval₂Hom_eq_bind₂ 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) : MvPolynomial.eval₂Hom f MvPolynomial.X = MvPolynomial.bind₂ f
• MvPolynomial.eval₂Hom_id_X_eq_join₂ 📋 Mathlib.Algebra.MvPolynomial.Monad
  (σ : Type u_1) (R : Type u_3) [CommSemiring R] : MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X = MvPolynomial.join₂
• MvPolynomial.eval₂Hom_comp_bind₂ 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) : (MvPolynomial.eval₂Hom f g).comp (MvPolynomial.bind₂ h) = MvPolynomial.eval₂Hom ((MvPolynomial.eval₂Hom f g).comp h) g

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 e668239 serving mathlib revision 15d4269