Loogle!

Result

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

• Polynomial.aeval 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : Polynomial R →ₐ[R] A
• Polynomial.aevalTower_id 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} [CommSemiring S] : Polynomial.aevalTower (AlgHom.id S S) = Polynomial.aeval
• Polynomial.aevalTower_ofId 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring S] [Algebra S A'] : Polynomial.aevalTower (Algebra.ofId S A') = Polynomial.aeval
• Polynomial.aeval_X 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (Polynomial.aeval x) Polynomial.X = x
• Polynomial.aeval_X_left 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] : Polynomial.aeval Polynomial.X = AlgHom.id R (Polynomial R)
• Polynomial.coe_aeval_eq_eval 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (r : R) : ⇑(Polynomial.aeval r) = Polynomial.eval r
• Polynomial.aeval_def 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (p : Polynomial R) : (Polynomial.aeval x) p = Polynomial.eval₂ (algebraMap R A) x p
• Polynomial.eval_map_algebraMap 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (P : Polynomial R) (b : B) : Polynomial.eval b (Polynomial.map (algebraMap R B) P) = (Polynomial.aeval b) P
• Polynomial.aeval_natCast 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (n : ℕ) : (Polynomial.aeval x) ↑n = ↑n
• Polynomial.aeval_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (Polynomial.aeval x) 0 = 0
• Polynomial.aeval_pi 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {I : Type u_3} {A : I → Type u_4} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : (i : I) → A i) : Polynomial.aeval x = AlgHom.pi fun i => Polynomial.aeval (x i)
• Polynomial.coeff_zero_eq_aeval_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p : Polynomial R) : p.coeff 0 = (Polynomial.aeval 0) p
• Polynomial.aeval_one 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (Polynomial.aeval x) 1 = 1
• Polynomial.aeval_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) (x : A) : Polynomial.aeval (f x) = f.comp (Polynomial.aeval x)
• Polynomial.aeval_algEquiv 📋 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) (x : A) : Polynomial.aeval (f x) = (↑f).comp (Polynomial.aeval x)
• Polynomial.aeval_prod 📋 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] (x : A × B) : Polynomial.aeval x = (Polynomial.aeval x.1).prod (Polynomial.aeval x.2)
• Polynomial.coeff_zero_eq_aeval_zero' 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) : (algebraMap R A) (p.coeff 0) = (Polynomial.aeval 0) p
• Polynomial.aeval_X_left_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p : Polynomial R) : (Polynomial.aeval Polynomial.X) p = p
• Polynomial.aeval_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : (Polynomial.aeval x) p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i
• Polynomial.isRoot_of_aeval_algebraMap_eq_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} {r : R} (hr : (Polynomial.aeval ((algebraMap R S) r)) p = 0) : p.IsRoot r
• Polynomial.aeval_X_pow 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} : (Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n
• Polynomial.aeval_eq_sum_range 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (x : S) : (Polynomial.aeval x) p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i
• Polynomial.comp_eq_aeval 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {p q : Polynomial R} : p.comp q = (Polynomial.aeval q) p
• Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : R) (p : Polynomial R) : (Polynomial.aeval ((algebraMap R A) x)) p = (algebraMap R A) (Polynomial.eval x p)
• Polynomial.aeval_X_left_eq_map 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Polynomial R) : (Polynomial.aeval Polynomial.X) p = Polynomial.map (algebraMap R S) p
• Polynomial.aeval_C 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) : (Polynomial.aeval x) (Polynomial.C r) = (algebraMap R A) r
• Polynomial.aeval_op_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (p : Polynomial R) : (Polynomial.aeval (MulOpposite.op x)) p = MulOpposite.op ((Polynomial.aeval x) p)
• Polynomial.aevalEquiv_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (Polynomial.aevalEquiv R A) x = Polynomial.aeval x
• Polynomial.aeval_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 : Type u_3} [FunLike F A B] [AlgHomClass F R A B] (f : F) (x : A) (p : Polynomial R) : (Polynomial.aeval (f x)) p = f ((Polynomial.aeval x) p)
• Polynomial.aeval_dvd 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial R} (x : A) (h : p ∣ q) : (Polynomial.aeval x) p ∣ (Polynomial.aeval x) q
• Polynomial.aeval_pi_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {I : Type u_3} {A : I → Type u_4} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : (i : I) → A i) (p : Polynomial R) : (Polynomial.aeval x) p = fun j => (Polynomial.aeval (x j)) p
• Polynomial.aeval_pi_apply₂ 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {I : Type u_3} {A : I → Type u_4} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : (i : I) → A i) (p : Polynomial R) (j : I) : (Polynomial.aeval x) p j = (Polynomial.aeval (x j)) p
• Polynomial.aeval_fn_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {X : Type u_3} (g : Polynomial R) (f : X → R) (x : X) : (Polynomial.aeval f) g x = (Polynomial.aeval (f x)) g
• Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {p q : Polynomial R} {x : B} (h₁ : p ∣ q) (h₂ : (Polynomial.aeval x) p = 0) : (Polynomial.aeval x) q = 0
• Polynomial.aeval_eq_aeval_map 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {S : Type v} {T : Type w} [CommSemiring R] [Semiring S] [CommSemiring T] [Algebra R S] [Algebra T S] {φ : R →+* T} (h : (algebraMap T S).comp φ = algebraMap R S) (p : Polynomial R) (a : S) : (Polynomial.aeval a) p = (Polynomial.aeval a) (Polynomial.map φ p)
• Polynomial.aeval_comp 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {p q : Polynomial R} {A : Type u_3} [Semiring A] [Algebra R A] (x : A) : (Polynomial.aeval x) (p.comp q) = (Polynomial.aeval ((Polynomial.aeval x) q)) p
• Polynomial.coe_aeval_eq_evalRingHom 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (x : R) : ↑(Polynomial.aeval x) = Polynomial.evalRingHom x
• Polynomial.aeval_neg 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommRing R] {p : Polynomial R} [Ring A] [Algebra R A] (x : A) : (Polynomial.aeval x) (-p) = -(Polynomial.aeval x) p
• Polynomial.aeval_monomial 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} {r : R} : (Polynomial.aeval x) ((Polynomial.monomial n) r) = (algebraMap R A) r * x ^ n
• Polynomial.aeval_add 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial R} (x : A) : (Polynomial.aeval x) (p + q) = (Polynomial.aeval x) p + (Polynomial.aeval x) q
• Polynomial.aeval_mul 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial R} (x : A) : (Polynomial.aeval x) (p * q) = (Polynomial.aeval x) p * (Polynomial.aeval x) q
• Polynomial.algEquivOfCompEqX_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = Polynomial.X) (hqp : q.comp p = Polynomial.X) (a : Polynomial R) : (p.algEquivOfCompEqX q hpq hqp) a = (Polynomial.aeval p) a
• Polynomial.aeval_prod_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] (x : A × B) (p : Polynomial R) : (Polynomial.aeval x) p = ((Polynomial.aeval x.1) p, (Polynomial.aeval x.2) p)
• Polynomial.map_aeval_eq_aeval_map 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] {S : Type u_3} {T : Type u_4} {U : Type u_5} [Semiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U} (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : Polynomial R) (a : S) : ψ ((Polynomial.aeval a) p) = (Polynomial.aeval (ψ a)) (Polynomial.map φ p)
• Polynomial.aeval_smul 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (f : Polynomial R) {G : Type u_3} [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A] (g : G) (x : A) : (Polynomial.aeval (g • x)) f = g • (Polynomial.aeval x) f
• Polynomial.algEquivAevalNegX_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (a : Polynomial R) : Polynomial.algEquivAevalNegX a = (Polynomial.aeval (-Polynomial.X)) a
• Polynomial.coe_aeval_mk_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) {S : Subalgebra R A} (h : x ∈ S) : ↑((Polynomial.aeval ⟨x, h⟩) p) = (Polynomial.aeval x) p
• Polynomial.aeval_subalgebra_coe 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommSemiring R] (g : Polynomial R) {A : Type u_3} [Semiring A] [Algebra R A] (s : Subalgebra R A) (f : ↥s) : ↑((Polynomial.aeval f) g) = (Polynomial.aeval ↑f) g
• Polynomial.aeval_sub 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} [CommRing R] {p q : Polynomial R} [Ring A] [Algebra R A] (x : A) : (Polynomial.aeval x) (p - q) = (Polynomial.aeval x) p - (Polynomial.aeval x) q
• Polynomial.algEquivAevalNegX_symm_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (a : Polynomial R) : Polynomial.algEquivAevalNegX.symm a = (Polynomial.aeval (-Polynomial.X)) a
• Polynomial.algEquivAevalXAddC_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (t : R) (a : Polynomial R) : (Polynomial.algEquivAevalXAddC t) a = (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a
• Polynomial.aeval_apply_smul_mem_of_le_comap 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {q : Submodule R M} {m : M} (hm : m ∈ q) (p : Polynomial R) (f : Module.End R M) (hq : q ≤ Submodule.comap f q) : ((Polynomial.aeval f) p) m ∈ q
• Polynomial.algEquivCMulXAddC_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (a b : R) [Invertible a] (a✝ : Polynomial R) : (Polynomial.algEquivCMulXAddC a b) a✝ = (Polynomial.aeval (Polynomial.C a * Polynomial.X + Polynomial.C b)) a✝
• Polynomial.aeval_apply_smul_mem_of_le_comap' 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} {A : Type z} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {q : Submodule R M} {m : M} [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (hm : m ∈ q) (p : Polynomial R) (a : A) (hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q) : (Polynomial.aeval a) p • m ∈ q
• Polynomial.algEquivCMulXAddC_symm_apply 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u_3} [CommRing R] (a b : R) [Invertible a] (a✝ : Polynomial R) : (Polynomial.algEquivCMulXAddC a b).symm a✝ = (Polynomial.aeval (Polynomial.C ⅟a * (Polynomial.X - Polynomial.C b))) a✝
• Polynomial.aeval_endomorphism 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {R : Type u} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) (p : Polynomial R) : ((Polynomial.aeval f) p) v = p.sum fun n b => b • (f ^ n) v
• Algebra.adjoin_singleton_eq_range_aeval 📋 Mathlib.RingTheory.Adjoin.Polynomial.Basic
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : R[x] = (Polynomial.aeval x).range
• Polynomial.aeval_mem_adjoin_singleton 📋 Mathlib.RingTheory.Adjoin.Polynomial.Basic
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) : (Polynomial.aeval x) p ∈ R[x]
• Algebra.instCoeDepCoeAlgHomPolynomialAevalSubtypeMemSubalgebraAdjoinSingletonSet 📋 Mathlib.RingTheory.Adjoin.Polynomial.Basic
  {A : Type u_2} {B : Type u_3} [CommSemiring A] [Semiring B] [Algebra A B] (x : B) (p : Polynomial A) : CoeDep B ((Polynomial.aeval x) p) ↥A[x]
• Algebra.adjoin_mem_exists_aeval 📋 Mathlib.RingTheory.Adjoin.Polynomial.Basic
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {a : A} (h : a ∈ R[x]) : ∃ p, (Polynomial.aeval x) p = a
• Algebra.adjoin_eq_exists_aeval 📋 Mathlib.RingTheory.Adjoin.Polynomial.Basic
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (a : ↥R[x]) : ∃ p, (Polynomial.aeval x) p = ↑a
• Algebra.adjoin_singleton_induction 📋 Mathlib.RingTheory.Adjoin.Polynomial.Basic
  (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {M : ↥R[x] → Prop} (a : ↥R[x]) (f : ∀ (p : Polynomial R), M ⟨(Polynomial.aeval x) p, ⋯⟩) : M a
• MvPolynomial.aeval_comp_toMvPolynomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] (f : σ → S) (i : σ) : (MvPolynomial.aeval f).comp (Polynomial.toMvPolynomial i) = Polynomial.aeval (f i)
• MvPolynomial.aeval_toMvPolynomial 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] (f : σ → S) (i : σ) (p : Polynomial R) : (MvPolynomial.aeval f) ((Polynomial.toMvPolynomial i) p) = (Polynomial.aeval (f i)) p
• MvPolynomial.rename_polynomial_aeval_X 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) [CommSemiring R] {σ : Type u_2} {τ : Type u_3} (f : σ → τ) (i : σ) (p : Polynomial R) : (MvPolynomial.rename f) ((Polynomial.aeval (MvPolynomial.X i)) p) = (Polynomial.aeval (MvPolynomial.X (f i))) p
• MvPolynomial.optionEquivRight_symm_apply 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) (S₁ : Type v) [CommSemiring R] (a : MvPolynomial S₁ (Polynomial R)) : (MvPolynomial.optionEquivRight R S₁).symm a = (MvPolynomial.aevalTower (Polynomial.aeval (MvPolynomial.X none)) fun i => MvPolynomial.X (some i)) a
• Polynomial.linearIndependent_powers_iff_aeval 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) : (LinearIndependent R fun n => (f ^ n) v) ↔ ∀ (p : Polynomial R), ((Polynomial.aeval f) p) v = 0 → p = 0
• Polynomial.disjoint_ker_aeval_of_isCoprime 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p q : Polynomial R} (hpq : IsCoprime p q) : Disjoint ((Polynomial.aeval f) p).ker ((Polynomial.aeval f) q).ker
• Polynomial.sup_aeval_range_eq_top_of_isCoprime 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p q : Polynomial R} (hpq : IsCoprime p q) : ((Polynomial.aeval f) p).range ⊔ ((Polynomial.aeval f) q).range = ⊤
• Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p q : Polynomial R} (hpq : IsCoprime p q) : ((Polynomial.aeval f) p).ker ⊔ ((Polynomial.aeval f) q).ker = ((Polynomial.aeval f) (p * q)).ker
• Polynomial.sup_ker_aeval_le_ker_aeval_mul 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : M →ₗ[R] M} {p q : Polynomial R} : ((Polynomial.aeval f) p).ker ⊔ ((Polynomial.aeval f) q).ker ≤ ((Polynomial.aeval f) (p * q)).ker
• Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} {S : Type v} [CommRing R] [Nontrivial R] [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : p.Monic) {x : S} (hx : (Polynomial.aeval x) p = 0) : 0 < p.natDegree
• Polynomial.aeval_ne_zero_of_isCoprime 📋 Mathlib.Algebra.Polynomial.RingDivision
  {S : Type v} {R : Type u_1} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S] {p q : Polynomial R} (h : IsCoprime p q) (s : S) : (Polynomial.aeval s) p ≠ 0 ∨ (Polynomial.aeval s) q ≠ 0
• Irreducible.aeval_ne_zero_of_natDegree_ne_one 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [Ring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : Irreducible p) (hdeg : p.natDegree ≠ 1) {x : S} (hx : x ∈ (algebraMap R S).range) : (Polynomial.aeval x) p ≠ 0
• Polynomial.natDegree_pos_of_aeval_root 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p ≠ 0) {z : S} (hz : (Polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) : 0 < p.natDegree
• Polynomial.degree_pos_of_aeval_root 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p ≠ 0) {z : S} (hz : (Polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) : 0 < p.degree
• Polynomial.aeval_modByMonic_eq_self_of_root 📋 Mathlib.Algebra.Polynomial.RingDivision
  {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {p q : Polynomial R} {x : S} (hx : (Polynomial.aeval x) q = 0) : (Polynomial.aeval x) (p %ₘ q) = (Polynomial.aeval x) p
• Polynomial.expand_aeval 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] {A : Type u_1} [Semiring A] [Algebra R A] (p : ℕ) (P : Polynomial R) (r : A) : (Polynomial.aeval r) ((Polynomial.expand R p) P) = (Polynomial.aeval (r ^ p)) P
• transcendental_iff 📋 Mathlib.RingTheory.Algebraic.Defs
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {x : A} : Transcendental R x ↔ ∀ (p : Polynomial R), (Polynomial.aeval x) p = 0 → p = 0
• Polynomial.aeval_map_algebraMap 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : B) (p : Polynomial R) : (Polynomial.aeval x) (Polynomial.map (algebraMap R A) p) = (Polynomial.aeval x) p
• Polynomial.aeval_algebraMap_apply 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} {A : Type u_2} (B : Type u_3) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : A) (p : Polynomial R) : (Polynomial.aeval ((algebraMap A B) x)) p = (algebraMap A B) ((Polynomial.aeval x) p)
• Polynomial.aeval_algebraMap_eq_zero_iff 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} {A : Type u_2} (B : Type u_3) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [IsDomain A] [Module.IsTorsionFree A B] [Nontrivial B] (x : A) (p : Polynomial R) : (Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0
• Polynomial.aeval_algebraMap_eq_zero_iff_of_injective 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} {p : Polynomial R} (h : Function.Injective ⇑(algebraMap A B)) : (Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0
• Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (s : Multiset A) {x : A} (hx : x ∈ s) {p : Polynomial R} (hp : (Polynomial.mapAlg R A) p = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) s).prod) : (Polynomial.aeval x) p = 0
• Subalgebra.aeval_coe 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (p : Polynomial R) : (Polynomial.aeval ↑x) p = ↑((Polynomial.aeval x) p)
• Polynomial.aeval_eq_zero_of_mem_rootSet 📋 Mathlib.Algebra.Polynomial.Roots
  {S : Type v} {T : Type w} [CommRing T] {p : Polynomial T} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (hx : a ∈ p.rootSet S) : (Polynomial.aeval a) p = 0
• Polynomial.Monic.mem_rootSet 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] {p : Polynomial T} (hp : p.Monic) {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] {a : S} : a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
• Polynomial.mem_roots_iff_aeval_eq_zero 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {x : R} (w : p ≠ 0) : x ∈ p.roots ↔ (Polynomial.aeval x) p = 0
• Polynomial.mem_aroots' 📋 Mathlib.Algebra.Polynomial.Roots
  {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {p : Polynomial T} {a : S} : a ∈ p.aroots S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
• Polynomial.mem_rootSet' 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] {a : S} : a ∈ p.rootSet S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
• Polynomial.mem_rootSet_of_ne 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [CommRing S] [IsDomain S] [Algebra T S] [Module.IsTorsionFree T S] (hp : p ≠ 0) {a : S} : a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
• Polynomial.mem_aroots 📋 Mathlib.Algebra.Polynomial.Roots
  {S : Type v} {T : Type w} [CommRing T] [IsDomain T] [CommRing S] [IsDomain S] [Algebra T S] [Module.IsTorsionFree T S] {p : Polynomial T} {a : S} : a ∈ p.aroots S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
• Polynomial.mem_rootSet 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [CommRing S] [IsDomain S] [Algebra T S] [Module.IsTorsionFree T S] {a : S} : a ∈ p.rootSet S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
• Polynomial.mem_rootSet_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommRing S] {p : Polynomial S} [Algebra S R] (h : Function.Injective ⇑(algebraMap S R)) {x : R} (hp : p ≠ 0) : x ∈ p.rootSet R ↔ (Polynomial.aeval x) p = 0
• Polynomial.aeval_primPart_eq_zero 📋 Mathlib.RingTheory.Polynomial.Content
  {R : Type u_1} [CommRing R] [NormalizedGCDMonoid R] {S : Type u_2} [Ring S] [IsDomain S] [Algebra R S] [Module.IsTorsionFree R S] {p : Polynomial R} {s : S} (hpzero : p ≠ 0) (hp : (Polynomial.aeval s) p = 0) : (Polynomial.aeval s) p.primPart = 0
• transcendental_iff_injective 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {x : A} : Transcendental R x ↔ Function.Injective ⇑(Polynomial.aeval x)
• isAlgebraic_iff_not_injective 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {x : A} : IsAlgebraic R x ↔ ¬Function.Injective ⇑(Polynomial.aeval x)
• Transcendental.of_aeval 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} {f : Polynomial R} (H : Transcendental R ((Polynomial.aeval r) f)) : Transcendental R f
• IsAlgebraic.of_aeval_of_transcendental 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} {f : Polynomial R} (H : IsAlgebraic R ((Polynomial.aeval r) f)) (hf : Transcendental R f) : IsAlgebraic R r
• Transcendental.aeval_of_transcendental 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} (H : Transcendental R r) {f : Polynomial R} (hf : Transcendental R f) : Transcendental R ((Polynomial.aeval r) f)
• IsAlgebraic.of_aeval 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} (f : Polynomial R) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) (H : IsAlgebraic R ((Polynomial.aeval r) f)) : IsAlgebraic R r
• Transcendental.aeval 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} (H : Transcendental R r) (f : Polynomial R) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) : Transcendental R ((Polynomial.aeval r) f)
• IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) : ∃ q, q.coeff 0 ≠ 0 ∧ (Polynomial.aeval s) q = 0
• transcendental_iff_ker_eq_bot 📋 Mathlib.RingTheory.Algebraic.Basic
  {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {x : A} : Transcendental R x ↔ RingHom.ker (Polynomial.aeval x) = ⊥
• inv_eq_of_root_of_coeff_zero_ne_zero 📋 Mathlib.RingTheory.Algebraic.Basic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} {p : Polynomial K} (aeval_eq : (Polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : x⁻¹ = -((Polynomial.aeval x) p.divX / (algebraMap K L) (p.coeff 0))
• inv_eq_of_aeval_divX_ne_zero 📋 Mathlib.RingTheory.Algebraic.Basic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} {p : Polynomial K} (aeval_ne : (Polynomial.aeval x) p.divX ≠ 0) : x⁻¹ = (Polynomial.aeval x) p.divX / ((Polynomial.aeval x) p - (algebraMap K L) (p.coeff 0))
• Polynomial.algEquivOfTranscendental_apply 📋 Mathlib.RingTheory.Algebraic.Basic
  (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) (f : Polynomial R) : (Polynomial.algEquivOfTranscendental R s h) f = (Polynomial.aeval ⟨s, ⋯⟩) f
• Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero 📋 Mathlib.RingTheory.Algebraic.Basic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (A : Subalgebra K L) {x : ↥A} {p : Polynomial K} (aeval_eq : (Polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : (↑x)⁻¹ ∈ A
• Polynomial.algEquivOfTranscendental_symm_aeval 📋 Mathlib.RingTheory.Algebraic.Basic
  (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) (f : Polynomial R) : (Polynomial.algEquivOfTranscendental R s h).symm ((Polynomial.aeval ⟨s, ⋯⟩) f) = f
• Polynomial.algEquivOfTranscendental_coe 📋 Mathlib.RingTheory.Algebraic.Basic
  (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (s : S) (h : Transcendental R s) : ↑(Polynomial.algEquivOfTranscendental R s h) = ↑(Polynomial.aeval ⟨s, ⋯⟩)
• PolyEquivTensor.toFunBilinear_apply_apply 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ((PolyEquivTensor.toFunBilinear R A) a) p = a • (Polynomial.aeval Polynomial.X) p
• Matrix.aeval_self_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
  {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) : (Polynomial.aeval M) M.charpoly = 0
• Polynomial.isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub 📋 Mathlib.RingTheory.Polynomial.Nilpotent
  {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {a b : S} (hb : IsUnit ((Polynomial.aeval b) P)) (hab : IsNilpotent (a - b)) : IsUnit ((Polynomial.aeval a) P)
• Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub 📋 Mathlib.RingTheory.Polynomial.Nilpotent
  {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Polynomial R) {a b : S} (h : IsNilpotent (a - b)) : IsNilpotent ((Polynomial.aeval a) P - (Polynomial.aeval b) P)
• Matrix.pow_eq_aeval_mod_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
  {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) (k : ℕ) : M ^ k = (Polynomial.aeval M) (Polynomial.X ^ k %ₘ M.charpoly)
• Matrix.aeval_eq_aeval_mod_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
  {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) (p : Polynomial R) : (Polynomial.aeval M) p = (Polynomial.aeval M) (p %ₘ M.charpoly)
• LinearMap.exists_monic_and_aeval_eq_zero 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) : ∃ p, p.Monic ∧ (Polynomial.aeval f) p = 0
• LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) : ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (Polynomial.aeval f) p = 0
• LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) : ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
• LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
  {M : Type u_2} [AddCommGroup M] (R : Type u_3) [CommRing R] [Module R M] [Module.Finite R M] (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) : ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
• IsIntegral.of_aeval_monic 📋 Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {p : Polynomial R} (monic : p.Monic) (deg : p.natDegree ≠ 0) (hx : IsIntegral R ((Polynomial.aeval x) p)) : IsIntegral R x
• Submodule.span_range_natDegree_eq_adjoin 📋 Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
  {R : Type u_6} {A : Type u_7} [CommRing R] [Semiring A] [Algebra R A] {x : A} {f : Polynomial R} (hf : f.Monic) (hfx : (Polynomial.aeval x) f = 0) : Submodule.span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule R[x]
• Polynomial.aeval_add_of_sq_eq_zero 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommRing S] [Algebra R S] (p : Polynomial R) (x y : S) (hy : y ^ 2 = 0) : (Polynomial.aeval (x + y)) p = (Polynomial.aeval x) p + (Polynomial.aeval x) (Polynomial.derivative p) * y
• Polynomial.Splits.aeval_eq_prod_aroots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] (hf : (Polynomial.map (algebraMap R A) f).Splits) (hm : f.Monic) (x : A) : (Polynomial.aeval x) f = (Multiset.map (fun x_1 => x - x_1) (f.aroots A)).prod
• Polynomial.Splits.aeval_eq_prod_aroots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R S) f).Splits) (x : S) : (Polynomial.aeval x) f = (algebraMap R S) f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) (f.aroots S)).prod
• Polynomial.scaleRoots_aeval_eq_zero 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} {a : A} {r : R} (ha : (Polynomial.aeval a) p = 0) : (Polynomial.aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0
• Polynomial.scaleRoots_aeval_smul 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [CommSemiring R] {S : Type u_5} [CommSemiring S] [Algebra S R] {p : Polynomial S} (r : R) (s : S) : (Polynomial.aeval (s • r)) (p.scaleRoots s) = s ^ p.natDegree • (Polynomial.aeval r) p
• Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} {K : Type u_4} [CommSemiring R] [Field K] [Algebra R K] (inj : Function.Injective ⇑(algebraMap R K)) {p : Polynomial R} {r s : R} (hr : (Polynomial.aeval ((algebraMap R K) r / (algebraMap R K) s)) p = 0) (hs : s ∈ nonZeroDivisors R) : (Polynomial.aeval ((algebraMap R K) r)) (p.scaleRoots s) = 0
• Polynomial.integralNormalization_aeval_smul 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {S : Type v} [CommSemiring S] {R : Type u_2} [CommSemiring R] [Algebra R S] {p : Polynomial R} (h : 1 ≤ p.natDegree) (x : S) : (Polynomial.aeval (p.leadingCoeff • x)) p.integralNormalization = p.leadingCoeff ^ (p.natDegree - 1) • (Polynomial.aeval x) p
• Polynomial.integralNormalization_aeval_eq_zero 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {S : Type v} {A : Type u_1} [CommSemiring S] [Semiring A] [Algebra S A] {f : Polynomial S} {z : A} (hz : (Polynomial.aeval z) f = 0) (inj : ∀ (x : S), (algebraMap S A) x = 0 → x = 0) : (Polynomial.aeval ((algebraMap S A) f.leadingCoeff * z)) f.integralNormalization = 0
• isIntegral_leadingCoeff_smul 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (p : Polynomial R) (x : S) [Algebra R S] (h : (Polynomial.aeval x) p = 0) : IsIntegral R (p.leadingCoeff • x)
• transcendental_aeval_iff 📋 Mathlib.RingTheory.Algebraic.Integral
  {K : Type u_1} {A : Type u_4} [Field K] [Ring A] [Algebra K A] {r : A} {f : Polynomial K} : Transcendental K ((Polynomial.aeval r) f) ↔ Transcendental K r ∧ Transcendental K f
• IsLocalization.integerNormalization_aeval_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'] [Algebra R R'] [Algebra S R'] [IsScalarTower R S R'] (p : Polynomial S) {x : R'} (hx : (Polynomial.aeval x) p = 0) : (Polynomial.aeval x) (IsLocalization.integerNormalization M p) = 0
• is_integral_localization_at_leadingCoeff 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_1} [CommRing R] {M : Submonoid R} {S : Type u_2} [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {x : S} (p : Polynomial R) (hp : (Polynomial.aeval x) p = 0) (hM : p.leadingCoeff ∈ M) : (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
• Derivation.map_aeval 📋 Mathlib.RingTheory.Derivation.Basic
  {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (P : Polynomial R) (x : A) : D ((Polynomial.aeval x) P) = (Polynomial.aeval x) (Polynomial.derivative P) • D x
• Module.AEval.annihilator_eq_ker_aeval 📋 Mathlib.Algebra.Polynomial.Module.AEval
  {R : Type u_3} {A : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [FaithfulSMul A M] : Module.annihilator (Polynomial R) (Module.AEval R M a) = RingHom.ker (Polynomial.aeval a)
• Module.AEval.annihilator_top_eq_ker_aeval 📋 Mathlib.Algebra.Polynomial.Module.AEval
  {R : Type u_3} {A : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [FaithfulSMul A M] : ⊤.annihilator = RingHom.ker (Polynomial.aeval a)
• Module.AEval.of_aeval_smul 📋 Mathlib.Algebra.Polynomial.Module.AEval
  {R : Type u_1} {A : Type u_3} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (f : Polynomial R) (m : M) : (Module.AEval.of R M a) ((Polynomial.aeval a) f • m) = f • (Module.AEval.of R M a) m
• Module.AEval.of_symm_smul 📋 Mathlib.Algebra.Polynomial.Module.AEval
  {R : Type u_1} {A : Type u_3} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (f : Polynomial R) (m : Module.AEval R M a) : (Module.AEval.of R M a).symm (f • m) = (Polynomial.aeval a) f • (Module.AEval.of R M a).symm m
• PolynomialModule.aeval_equivPolynomial 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} [CommRing R] {S : Type u_8} [CommRing S] [Algebra S R] (f : PolynomialModule S S) (x : R) : (Polynomial.aeval x) (PolynomialModule.equivPolynomial f) = (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap S R)) f)
• PolynomialModule.smul_def 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f : Polynomial R) (m : PolynomialModule R M) : f • m = ((Polynomial.aeval (↑(PolynomialModule.coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(PolynomialModule.coeffLinearEquiv R R))) f) m
• IntermediateField.aeval_coe 📋 Mathlib.FieldTheory.IntermediateField.Basic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [CommSemiring R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] (x : ↥S) (P : Polynomial R) : (Polynomial.aeval ↑x) P = ↑((Polynomial.aeval x) P)
• Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommRing R] {𝓟 : Ideal R} {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] (hf : f.IsWeaklyEisensteinAt 𝓟) {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (i : ℕ) : (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
• Polynomial.dvd_pow_natDegree_of_aeval_eq_zero 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} {A : Type u_1} [CommRing R] [CommRing A] [IsDomain R] [Algebra R A] [Nontrivial A] [Module.IsTorsionFree R A] {p : Polynomial R} (hp : p.Monic) (x y : R) (z : A) (h : (Polynomial.aeval z) p = 0) (hz : z * (algebraMap R A) x = (algebraMap R A) y) : x ∣ y ^ p.natDegree
• Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (hf : f.IsWeaklyEisensteinAt (R ∙ p)) : ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
• Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (hf : f.IsWeaklyEisensteinAt (R ∙ p)) (i : ℕ) : (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i
• minpoly.aeval 📋 Mathlib.FieldTheory.Minpoly.Basic
  (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) : (Polynomial.aeval x) (minpoly A x) = 0
• minpoly.min 📋 Mathlib.FieldTheory.Minpoly.Basic
  (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pmonic : p.Monic) (hp : (Polynomial.aeval x) p = 0) : (minpoly A x).degree ≤ p.degree
• minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly 📋 Mathlib.FieldTheory.Minpoly.Basic
  {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} {a : Polynomial A} (hx : IsIntegral A x) (hamonic : a.Monic) (hdvd : DvdNotUnit a (minpoly A x)) : (Polynomial.aeval x) a ≠ 0
• minpoly.aeval_algHom 📋 Mathlib.FieldTheory.Minpoly.Basic
  (A : Type u_1) {B : Type u_2} {B' : Type u_3} [CommRing A] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B →ₐ[A] B') (x : B) : (Polynomial.aeval (f x)) (minpoly A x) = 0
• minpoly.eq_of_linearIndependent 📋 Mathlib.FieldTheory.Minpoly.Basic
  (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (monic : p.Monic) (hp0 : (Polynomial.aeval x) p = 0) (n : ℕ) (hpn : p.degree = ↑n) (ind : LinearIndependent A fun i => x ^ ↑i) : minpoly A x = p
• minpoly.aeval_modByMonic_minpoly 📋 Mathlib.FieldTheory.Minpoly.Basic
  {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (p : Polynomial A) (x : B) : (Polynomial.aeval x) (p %ₘ minpoly A x) = (Polynomial.aeval x) p
• minpoly.unique' 📋 Mathlib.FieldTheory.Minpoly.Basic
  (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (hm : p.Monic) (hp : (Polynomial.aeval x) p = 0) (hl : ∀ (q : Polynomial A), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0) : p = minpoly A x
• minpoly.eq_iff_aeval_minpoly_eq_zero 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] [IsDomain B] {C : Type u_3} [Ring C] [Algebra A C] [Nontrivial C] {b : B} (h : IsIntegral A b) {c : C} : minpoly A b = minpoly A c ↔ (Polynomial.aeval c) (minpoly A b) = 0
• minpoly.eq_of_irreducible_of_monic 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] {p : Polynomial A} (hp1 : Irreducible p) (hp2 : (Polynomial.aeval x) p = 0) (hp3 : p.Monic) : p = minpoly A x
• minpoly.eq_iff_aeval_eq_zero 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] {p : Polynomial A} (irr : Irreducible p) (monic : p.Monic) : p = minpoly A x ↔ (Polynomial.aeval x) p = 0
• minpoly.unique_of_degree_le_degree_minpoly 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pmonic : p.Monic) (hp : (Polynomial.aeval x) p = 0) (pmin : p.degree ≤ (minpoly A x).degree) : p = minpoly A x
• minpoly.degree_le_of_ne_zero 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pnz : p ≠ 0) (hp : (Polynomial.aeval x) p = 0) : (minpoly A x).degree ≤ p.degree
• minpoly.dvd 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (hp : (Polynomial.aeval x) p = 0) : minpoly A x ∣ p
• minpoly.dvd_iff 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} {p : Polynomial A} : minpoly A x ∣ p ↔ (Polynomial.aeval x) p = 0
• minpoly.Irreducible.eq_minpoly 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] {p : Polynomial A} (hi : Irreducible p) (hx : (Polynomial.aeval x) p = 0) : p = Polynomial.C p.leadingCoeff * minpoly A x
• minpoly.eq_of_irreducible 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] {p : Polynomial A} (hp1 : Irreducible p) (hp2 : (Polynomial.aeval x) p = 0) : p * Polynomial.C p.leadingCoeff⁻¹ = minpoly A x
• minpoly.unique 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pmonic : p.Monic) (hp : (Polynomial.aeval x) p = 0) (pmin : ∀ (q : Polynomial A), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree) : p = minpoly A x
• minpoly.aeval_of_isScalarTower 📋 Mathlib.FieldTheory.Minpoly.Field
  (R : Type u_3) {K : Type u_4} {T : Type u_5} {U : Type u_6} [CommRing R] [Field K] [CommRing T] [Algebra R K] [Algebra K T] [Algebra R T] [IsScalarTower R K T] [CommSemiring U] [Algebra K U] [Algebra R U] [IsScalarTower R K U] (x : T) (y : U) (hy : (Polynomial.aeval y) (minpoly K x) = 0) : (Polynomial.aeval y) (minpoly R x) = 0
• Irreducible.dvd_iff_aeval_eq_zero 📋 Mathlib.FieldTheory.Minpoly.Field
  {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] [Nontrivial B] {p q : Polynomial A} (hi : Irreducible p) {b : B} (hfa : (Polynomial.aeval b) p = 0) : (Polynomial.aeval b) q = 0 ↔ p ∣ q
• minpoly.ker_aeval_eq_span_minpoly 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) : RingHom.ker (Polynomial.aeval x) = Polynomial A ∙ minpoly A x
• PowerBasis.exists_eq_aeval' 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) (y : S) : ∃ f, y = (Polynomial.aeval pb.gen) f
• PowerBasis.aeval_minpolyGen 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (pb : PowerBasis A S) : (Polynomial.aeval pb.gen) pb.minpolyGen = 0
• PowerBasis.exists_eq_aeval 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) (y : S) : ∃ f, f.natDegree < pb.dim ∧ y = (Polynomial.aeval pb.gen) f
• PowerBasis.lift 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) : S →ₐ[A] S'
• PowerBasis.liftEquiv 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) : (S →ₐ[A] S') ≃ { y // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }
• PowerBasis.dim_le_natDegree_of_root 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (pb : PowerBasis A S) {p : Polynomial A} (ne_zero : p ≠ 0) (root : (Polynomial.aeval pb.gen) p = 0) : pb.dim ≤ p.natDegree
• PowerBasis.dim_le_degree_of_root 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] (h : PowerBasis A S) {p : Polynomial A} (ne_zero : p ≠ 0) (root : (Polynomial.aeval h.gen) p = 0) : ↑h.dim ≤ p.degree
• PowerBasis.lift_gen 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) : (pb.lift y hy) pb.gen = y
• PowerBasis.mem_span_pow 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x y : S} {d : ℕ} (hd : d ≠ 0) : y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (Polynomial.aeval x) f
• PowerBasis.mem_span_pow' 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x y : S} {d : ℕ} : y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (Polynomial.aeval x) f
• IsIntegral.mem_span_pow 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial R] {x y : S} (hx : IsIntegral R x) (hy : ∃ f, y = (Polynomial.aeval x) f) : y ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
• PowerBasis.equivOfRoot 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) : S ≃ₐ[A] S'
• PowerBasis.equivOfMinpoly_aeval 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) (f : Polynomial A) : (pb.equivOfMinpoly pb' h) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
• PowerBasis.equivOfRoot_symm 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) : (pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁
• PowerBasis.equivOfRoot_gen 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) : (pb.equivOfRoot pb' h₁ h₂) pb.gen = pb'.gen
• PowerBasis.equivOfRoot_map 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] {S' : Type u_6} [CommRing S'] [Algebra A S] [Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A (pb.map e).gen) = 0) (h₂ : (Polynomial.aeval (pb.map e).gen) (minpoly A pb.gen) = 0) : pb.equivOfRoot (pb.map e) h₁ h₂ = e
• PowerBasis.equivOfRoot_apply 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (a : S) : (pb.equivOfRoot pb' h₁ h₂) a = (pb.lift pb'.gen h₂) a
• PowerBasis.lift_aeval 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : S') (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A) : (pb.lift y hy) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
• PowerBasis.equivOfRoot_aeval 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0) (f : Polynomial A) : (pb.equivOfRoot pb' h₁ h₂) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
• PowerBasis.liftEquiv_apply_coe 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (f : S →ₐ[A] S') : ↑(pb.liftEquiv f) = f pb.gen
• PowerBasis.liftEquiv_symm_apply 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) (y : { y // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }) : pb.liftEquiv.symm y = pb.lift ↑y ⋯
• PowerBasis.constr_pow_gen 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) : ((pb.basis.constr A) fun i => y ^ ↑i) pb.gen = y
• PowerBasis.constr_pow_algebraMap 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (x : A) : ((pb.basis.constr A) fun i => y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x
• PowerBasis.constr_pow_aeval 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A) : ((pb.basis.constr A) fun i => y ^ ↑i) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
• PowerBasis.constr_pow_mul 📋 Mathlib.RingTheory.PowerBasis
  {S : Type u_2} [Ring S] {A : Type u_3} [CommRing A] [Algebra A S] {S' : Type u_6} [Ring S'] [Algebra A S'] (pb : PowerBasis A S) {y : S'} (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (x x' : S) : ((pb.basis.constr A) fun i => y ^ ↑i) (x * x') = ((pb.basis.constr A) fun i => y ^ ↑i) x * ((pb.basis.constr A) fun i => y ^ ↑i) x'
• Algebra.mem_ideal_map_adjoin 📋 Mathlib.RingTheory.Polynomial.Ideal
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (x : S) (I : Ideal R) {y : ↥R[x]} : y ∈ Ideal.map (algebraMap R ↥R[x]) I ↔ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (Polynomial.aeval x) p = ↑y
• Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top 📋 Mathlib.RingTheory.Polynomial.Ideal
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) (I : Ideal R) (hI : I ≠ ⊤) [Invertible x] (h : Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤) : ∃ p, p.leadingCoeff - 1 ∈ I ∧ (Polynomial.aeval ⅟x) p = 0
• AdjoinRoot.aeval_algHom_eq_zero 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} {S : Type u_2} [CommRing R] (f : Polynomial R) [CommRing S] [Algebra R S] (ϕ : AdjoinRoot f →ₐ[R] S) : (Polynomial.aeval (ϕ (AdjoinRoot.root f))) f = 0
• AdjoinRoot.aeval_eq 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} [CommRing R] {f : Polynomial R} (p : Polynomial R) : (Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) p
• AdjoinRoot.aeval_eq_of_algebra 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial S) (p : Polynomial R) : (Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) (Polynomial.map (algebraMap R S) p)
• AdjoinRoot.equiv' 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : AdjoinRoot g ≃ₐ[R] S
• AdjoinRoot.equiv'_toAlgHom 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ↑(AdjoinRoot.equiv' g pb h₁ h₂) = AdjoinRoot.liftAlgHom g (Algebra.ofId R S) pb.gen h₂
• AdjoinRoot.equiv'_symm_toAlgHom 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ↑(AdjoinRoot.equiv' g pb h₁ h₂).symm = pb.lift (AdjoinRoot.root g) h₁
• AdjoinRoot.equiv'_apply 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (g : Polynomial R) (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) : ⇑(AdjoinRoot.equiv' g pb h₁ h₂) = ⇑(AdjoinRoot.liftAlgHom g (Algebra.ofId R S) pb.gen h₂)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59