Loogle!

Result

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

• 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₂_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₂_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₂_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₂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₂_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₂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₂_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₂_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_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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₂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₂_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₂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₂_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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₂_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.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.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.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₂_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₂_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₂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₂_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₂_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₂_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₂_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₂_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₂_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₂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.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₂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₂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₂_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.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.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₂_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₂_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.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.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₂_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₂_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₂_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.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.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₂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₂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₂_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.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_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₂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₂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₂_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_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₂_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₂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.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₂_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.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₂.eq_1 📋 Mathlib.Algebra.MvPolynomial.Rename
  {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 = Finsupp.sum p fun s a => f a * s.prod fun n e => g n ^ e
• 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_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
• 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
• 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
• 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.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} (hq : q.Monic) {x : S} (hx : Polynomial.eval₂ f x q = 0) : Polynomial.eval₂ f x (p %ₘ q) = Polynomial.eval₂ f x p
• 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}
• 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
• 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)
• 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.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₂_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 📋 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_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
• 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
• normalizeScaleRoots_eval₂_leadingCoeff_mul 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {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
• 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.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] [IsDomain 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
• 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
• 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
• MvPolynomial.eval₂Hom_C_id_eq_join₁ 📋 Mathlib.Algebra.MvPolynomial.Monad
  (σ : Type u_1) (R : Type u_3) [CommSemiring R] (φ : MvPolynomial (MvPolynomial σ R) R) : (MvPolynomial.eval₂Hom MvPolynomial.C id) φ = MvPolynomial.join₁ φ
• MvPolynomial.eval₂Hom_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 σ R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₂ h) φ) = (MvPolynomial.eval₂Hom ((MvPolynomial.eval₂Hom f g).comp h) g) φ
• MvPolynomial.eval₂Hom_bind₁ 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : τ → S) (h : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₁ h) φ) = (MvPolynomial.eval₂Hom f fun i => (MvPolynomial.eval₂Hom f g) (h i)) φ
• MvPolynomial.eval₂Hom_C_eq_bind₁ 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) : MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)
• MvPolynomial.eval₂Hom_C_left 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) : MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)
• MvPolynomial.IsHomogeneous.eval₂ 📋 Mathlib.RingTheory.MvPolynomial.Homogeneous
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {m n : ℕ} (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (hf : ∀ (r : R), (f r).IsHomogeneous 0) (hg : ∀ (i : σ), (g i).IsHomogeneous n) : (MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
• Matrix.charpoly.univ_map_eval₂Hom 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
  {R : Type u_1} {S : Type u_2} (n : Type u_3) [CommRing R] [CommRing S] [Fintype n] [DecidableEq n] (f : R →+* S) (M : n × n → S) : Polynomial.map (MvPolynomial.eval₂Hom f M) (Matrix.charpoly.univ R n) = (Matrix.of (Function.curry M)).charpoly
• Matrix.charpoly.univ_coeff_eval₂Hom 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
  {R : Type u_1} {S : Type u_2} (n : Type u_3) [CommRing R] [CommRing S] [Fintype n] [DecidableEq n] (f : R →+* S) (M : n × n → S) (i : ℕ) : (MvPolynomial.eval₂Hom f M) ((Matrix.charpoly.univ R n).coeff i) = (Matrix.of (Function.curry M)).charpoly.coeff i
• Polynomial.eval₂RingHom'.eq_1 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (hf : ∀ (a : R), Commute (f a) x) : Polynomial.eval₂RingHom' f x hf = { toFun := Polynomial.eval₂ f x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
• 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
• 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
• 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
• AdjoinRoot.eval₂_root 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u} [CommRing R] (f : Polynomial R) : Polynomial.eval₂ (AdjoinRoot.of f) (AdjoinRoot.root f) f = 0
• IsAlgClosed.exists_eval₂_eq_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] {R : Type u_1} [DivisionRing 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.polynomial_eval_eval₂ 📋 Mathlib.Algebra.MvPolynomial.Polynomial
  {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] {x : S} (f : R →+* Polynomial S) (g : σ → Polynomial S) (p : MvPolynomial σ R) : Polynomial.eval x (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p
• Polynomial.eval₂_evalRingHom 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} [CommSemiring R] (x : R) : Polynomial.eval₂ (Polynomial.evalRingHom x) = Polynomial.evalEval x
• Polynomial.eval₂_eval₂RingHom_apply 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x y : S) (p : Polynomial (Polynomial R)) : Polynomial.eval₂ (Polynomial.eval₂RingHom f x) y p = Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom f) p)
• Polynomial.eval₂RingHom_eval₂RingHom 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x y : S) : Polynomial.eval₂RingHom (Polynomial.eval₂RingHom f x) y = (Polynomial.evalEvalRingHom x y).comp (Polynomial.mapRingHom (Polynomial.mapRingHom f))
• Polynomial.eval_C_X_eval₂_map_C_X 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} [CommSemiring R] {p : Polynomial (Polynomial R)} : Polynomial.eval (Polynomial.C Polynomial.X) (Polynomial.eval₂ (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (Polynomial.C Polynomial.X) p) = p
• Polynomial.eval_C_X_comp_eval₂_map_C_X 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} [CommSemiring R] : (Polynomial.evalRingHom (Polynomial.C Polynomial.X)).comp (Polynomial.eval₂RingHom (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (Polynomial.C Polynomial.X)) = RingHom.id (Polynomial (Polynomial R))
• Polynomial.eval₂_smulOneHom_eq_smeval 📋 Mathlib.Algebra.Polynomial.Smeval
  (R : Type u_3) [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [IsScalarTower R S S] (p : Polynomial R) (x : S) : Polynomial.eval₂ RingHom.smulOneHom x p = p.smeval x
• Polynomial.int_eval₂_eq 📋 Mathlib.Algebra.Ring.Subring.IntPolynomial
  {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) {L : Type u_2} [Field L] [Algebra K L] (x : L) : Polynomial.eval₂ (algebraMap (↥R) L) x (Polynomial.int R P hP) = (Polynomial.aeval x) P
• 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
• IsSepClosed.exists_eval₂_eq_zero 📋 Mathlib.FieldTheory.IsSepClosed
  {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed K] (f : k →+* K) (p : Polynomial k) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x, Polynomial.eval₂ f x p = 0
• Polynomial.continuous_eval₂ 📋 Mathlib.Topology.Algebra.Polynomial
  {R : Type u_1} {S : Type u_2} [Semiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [Semiring S] (p : Polynomial S) (f : S →+* R) : Continuous fun x => Polynomial.eval₂ f x p
• Polynomial.tendsto_abv_eval₂_atTop 📋 Mathlib.Topology.Algebra.Polynomial
  {R : Type u_1} {S : Type u_2} {k : Type u_3} {α : Type u_4} [Semiring R] [Ring S] [Field k] [LinearOrder k] [IsStrictOrderedRing k] (f : R →+* S) (abv : S → k) [IsAbsoluteValue abv] (p : Polynomial R) (hd : 0 < p.degree) (hf : f p.leadingCoeff ≠ 0) {l : Filter α} {z : α → S} (hz : Filter.Tendsto (abv ∘ z) l Filter.atTop) : Filter.Tendsto (fun x => abv (Polynomial.eval₂ f (z x) p)) l Filter.atTop

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 19971e9 serving mathlib revision 3008304