Loogle!

Result

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

• Polynomial.map 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial R → Polynomial S
• Polynomial.map_X 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f Polynomial.X = Polynomial.X
• Polynomial.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 x (Polynomial.map f p) = Polynomial.eval₂ f x p
• 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.map_natCast 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ℕ) : Polynomial.map f ↑n = ↑n
• Polynomial.map_one 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f 1 = 1
• Polynomial.map_zero 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f 0 = 0
• Polynomial.map_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p q : Polynomial R) : Polynomial.map f (p.comp q) = (Polynomial.map f p).comp (Polynomial.map f q)
• Polynomial.map_intCast 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {S : Type u_1} [Ring S] (f : R →+* S) (n : ℤ) : Polynomial.map f ↑n = ↑n
• Polynomial.map_ofNat 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] : Polynomial.map f (OfNat.ofNat n) = OfNat.ofNat n
• Polynomial.map.eq_1 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f = Polynomial.eval₂ (Polynomial.C.comp f) Polynomial.X
• Polynomial.map_list_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (L : List (Polynomial R)) : Polynomial.map f L.prod = (List.map (Polynomial.map f) L).prod
• Polynomial.map_neg 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) : Polynomial.map f (-p) = -Polynomial.map f p
• Polynomial.map_add 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [Semiring S] (f : R →+* S) : Polynomial.map f (p + q) = Polynomial.map f p + Polynomial.map f q
• Polynomial.map_mul 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [Semiring S] (f : R →+* S) : Polynomial.map f (p * q) = Polynomial.map f p * Polynomial.map f q
• Polynomial.map_dvd 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {x y : Polynomial R} : x ∣ y → Polynomial.map f x ∣ Polynomial.map f y
• Polynomial.coe_mapRingHom 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : ⇑(Polynomial.mapRingHom f) = Polynomial.map f
• Polynomial.map_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {ι : Type u_1} (g : ι → Polynomial R) (s : Finset ι) : Polynomial.map f (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.map f (g i)
• Polynomial.map_multiset_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (m : Multiset (Polynomial R)) : Polynomial.map f m.prod = (Multiset.map (Polynomial.map f) m).prod
• Polynomial.map_prod 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) {ι : Type u_1} (g : ι → Polynomial R) (s : Finset ι) : Polynomial.map f (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.map f (g i)
• Polynomial.map_pow 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (n : ℕ) : Polynomial.map f (p ^ n) = Polynomial.map f p ^ n
• Polynomial.map_sub 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Ring R] {p q : Polynomial R} {S : Type u_1} [Ring S] (f : R →+* S) : Polynomial.map f (p - q) = Polynomial.map f p - Polynomial.map f q
• Polynomial.map_C 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} {a : R} [Semiring R] [Semiring S] (f : R →+* S) : Polynomial.map f (Polynomial.C a) = Polynomial.C (f a)
• Polynomial.map_monomial 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {n : ℕ} {a : R} : Polynomial.map f ((Polynomial.monomial n) a) = (Polynomial.monomial n) (f a)
• Polynomial.map_id 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} [Semiring R] {p : Polynomial R} : Polynomial.map (RingHom.id R) p = p
• Polynomial.support_map_subset 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : (Polynomial.map f p).support ⊆ p.support
• Polynomial.map_injective 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Injective ⇑f) : Function.Injective (Polynomial.map f)
• Polynomial.map_surjective 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) : Function.Surjective (Polynomial.map f)
• Polynomial.map_injective_iff 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Function.Injective (Polynomial.map f) ↔ Function.Injective ⇑f
• Polynomial.map_surjective_iff 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) : Function.Surjective (Polynomial.map f) ↔ Function.Surjective ⇑f
• Polynomial.coeff_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (n : ℕ) : (Polynomial.map f p).coeff n = f (p.coeff n)
• Polynomial.support_map_of_injective 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) {f : R →+* S} (hf : Function.Injective ⇑f) : (Polynomial.map f p).support = p.support
• Polynomial.coeff_map_eq_comp 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : (Polynomial.map f p).coeff = ⇑f ∘ p.coeff
• Polynomial.map_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] (f : R →+* S) [Semiring T] (g : S →+* T) (p : Polynomial R) : Polynomial.map g (Polynomial.map f p) = Polynomial.map (g.comp f) 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.IsRoot.map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f : R →+* S} {x : R} {p : Polynomial R} (h : p.IsRoot x) : (Polynomial.map f p).IsRoot (f x)
• Polynomial.eval_natCast_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ) : Polynomial.eval (↑n) (Polynomial.map f p) = f (Polynomial.eval (↑n) p)
• Polynomial.eval_one_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : Polynomial.eval 1 (Polynomial.map f p) = f (Polynomial.eval 1 p)
• Polynomial.eval_zero_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : Polynomial.eval 0 (Polynomial.map f p) = f (Polynomial.eval 0 p)
• Polynomial.map_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) : Polynomial.map f p = 0 ↔ p = 0
• Polynomial.map_ne_zero_iff 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) : Polynomial.map f p ≠ 0 ↔ p ≠ 0
• Polynomial.eval_intCast_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (p : Polynomial R) (i : ℤ) : Polynomial.eval (↑i) (Polynomial.map f p) = f (Polynomial.eval (↑i) p)
• Polynomial.IsRoot.of_map 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {S : Type v} [CommSemiring S] {R : Type u_1} [Ring R] {f : R →+* S} {x : R} {p : Polynomial R} (h : (Polynomial.map f p).IsRoot (f x)) (hf : Function.Injective ⇑f) : p.IsRoot x
• Polynomial.isRoot_map_iff 📋 Mathlib.Algebra.Polynomial.Eval.Coeff
  {S : Type v} [CommSemiring S] {R : Type u_1} [CommRing R] {f : R →+* S} {x : R} {p : Polynomial R} (hf : Function.Injective ⇑f) : (Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x
• Polynomial.natDegree_map_le 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).natDegree ≤ p.natDegree
• Polynomial.degree_map_le 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).degree ≤ p.degree
• Polynomial.map_monic_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : p.Monic) [Nontrivial S] : Polynomial.map f p ≠ 0
• Polynomial.natDegree_map_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map_eq_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).degree = p.degree
• Polynomial.map_monic_eq_zero_iff 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : p.Monic) : Polynomial.map f p = 0 ↔ ∀ (x : R), f x = 0
• Polynomial.natDegree_map_lt' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : 0 < p.natDegree) : (Polynomial.map f p).natDegree < p.natDegree
• Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : IsUnit f.leadingCoeff) (H : IsUnit (Polynomial.map φ f)) : IsUnit f
• Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.degree_map_lt 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (Polynomial.map f p).degree < p.degree
• Polynomial.natDegree_map_lt 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : Polynomial.map f p ≠ 0) : (Polynomial.map f p).natDegree < p.natDegree
• Polynomial.mapEquiv_apply 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial R) : (Polynomial.mapEquiv e) a = Polynomial.map (↑e) a
• Polynomial.mapEquiv_symm_apply 📋 Mathlib.Algebra.Polynomial.Eval.Degree
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial S) : (Polynomial.mapEquiv e).symm a = Polynomial.map (↑e.symm) a
• Polynomial.coe_mapAlgHom 📋 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.map ↑f
• Polynomial.coe_mapAlgEquiv 📋 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.mapAlgEquiv f) = Polynomial.map ↑f
• 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.natDegree_map_eq_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
• Polynomial.degree_map_eq_iff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0
• MvPolynomial.coeff_eval_eq_eval_coeff 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} (S₁ : Type v) [CommSemiring R] (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R)) (i : ℕ) : (Polynomial.map (MvPolynomial.eval s') f).coeff i = (MvPolynomial.eval s') (f.coeff i)
• MvPolynomial.optionEquivLeft_elim_eval 📋 Mathlib.Algebra.MvPolynomial.Equiv
  (R : Type u) (S₁ : Type v) [CommSemiring R] (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R) : (MvPolynomial.eval fun x => x.elim y s) f = Polynomial.eval y (Polynomial.map (MvPolynomial.eval s) ((MvPolynomial.optionEquivLeft R S₁) f))
• MvPolynomial.eval_eq_eval_mv_eval' 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} [CommSemiring R] {n : ℕ} (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) : (MvPolynomial.eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (MvPolynomial.eval s) ((MvPolynomial.finSuccEquiv R n) f))
• MvPolynomial.finSuccEquiv_rename_finSuccEquiv 📋 Mathlib.Algebra.MvPolynomial.Equiv
  {R : Type u} {σ : Type u_1} [CommSemiring R] {n : ℕ} (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) : (MvPolynomial.finSuccEquiv R n) ((MvPolynomial.rename ⇑(e.optionCongr.trans (finSuccEquiv n).symm)) φ) = Polynomial.map (MvPolynomial.rename ⇑e).toRingHom ((MvPolynomial.optionEquivLeft R σ) φ)
• Polynomial.reflect_map 📋 Mathlib.Algebra.Polynomial.Reverse
  {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ) : Polynomial.reflect n (Polynomial.map f p) = Polynomial.map f (Polynomial.reflect n p)
• Polynomial.Monic.map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hp : p.Monic) : (Polynomial.map f p).Monic
• Polynomial.Monic.natDegree_map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).natDegree = P.natDegree
• Polynomial.Monic.degree_map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : P.Monic) (f : R →+* S) : (Polynomial.map f P).degree = P.degree
• Polynomial.monic_of_injective 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {p : Polynomial R} (hp : (Polynomial.map f p).Monic) : p.Monic
• Function.Injective.monic_map_iff 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {p : Polynomial R} : p.Monic ↔ (Polynomial.map f p).Monic
• Polynomial.natDegree_map_eq_of_injective 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map_eq_of_injective 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).degree = p.degree
• Polynomial.Monic.eq_one_of_map_eq_one 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic) (map_eq : Polynomial.map f p = 1) : p = 1
• Polynomial.leadingCoeff_map' 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.leadingCoeff_of_injective 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.nextCoeff_map 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : (Polynomial.map f p).nextCoeff = f p.nextCoeff
• Polynomial.map_toSubring 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : Polynomial.map T.subtype (p.toSubring T hp) = p
• Polynomial.map_restriction 📋 Mathlib.RingTheory.Polynomial.Basic
  {R : Type u} [CommRing R] (p : Polynomial R) : Polynomial.map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction = p
• Polynomial.derivative_map 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : Polynomial.derivative (Polynomial.map f p) = Polynomial.map f (Polynomial.derivative p)
• Polynomial.iterate_derivative_map 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) (k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.map f p) = Polynomial.map f ((⇑Polynomial.derivative)^[k] p)
• Polynomial.derivativeFinsupp_map 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : Polynomial.derivativeFinsupp (Polynomial.map f p) = Finsupp.mapRange (fun x => Polynomial.map f x) ⋯ (Polynomial.derivativeFinsupp p)
• Polynomial.map_divByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) : Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q
• Polynomial.map_modByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) : Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
• Polynomial.map_mod_divByMonic 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) : Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q ∧ Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
• Polynomial.map_dvd_map 📋 Mathlib.Algebra.Polynomial.Div
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Injective ⇑f) {x y : Polynomial R} (hx : x.Monic) : Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y
• Polynomial.map_contract 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] {p : ℕ} (hp : p ≠ 0) {f : R →+* S} {q : Polynomial R} : Polynomial.map f (Polynomial.contract p q) = Polynomial.contract p (Polynomial.map f q)
• Polynomial.expand_char 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (f : Polynomial R) : Polynomial.map (frobenius R p) ((Polynomial.expand R p) f) = f ^ p
• Polynomial.map_expand 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] {p : ℕ} {f : R →+* S} {q : Polynomial R} : Polynomial.map f ((Polynomial.expand R p) q) = (Polynomial.expand S p) (Polynomial.map f q)
• Polynomial.map_expand_pow_char 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (f : Polynomial R) (n : ℕ) : Polynomial.map (frobenius R p ^ n) ((Polynomial.expand R (p ^ n)) f) = f ^ p ^ n
• Polynomial.aroots_def 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : p.aroots S = (Polynomial.map (algebraMap T S) p).roots
• Polynomial.aroots.eq_1 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] : p.aroots S = (Polynomial.map (algebraMap T S) p).roots
• Polynomial.bUnion_roots_finite 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ℕ) {U : Set R} (h : U.Finite) : (⋃ f, ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).Finite
• Polynomial.card_roots_le_map_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) : p.roots.card ≤ (Polynomial.map f p).roots.card
• Polynomial.card_roots_le_map 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p ≠ 0) : p.roots.card ≤ (Polynomial.map f p).roots.card
• Polynomial.mem_roots_map_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [Semiring S] {p : Polynomial S} {f : S →+* R} (hf : Function.Injective ⇑f) {x : R} (hp : p ≠ 0) : x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0
• Polynomial.Monic.roots_map_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} (hm : p.Monic) (f : A →+* B) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• Polynomial.aroots_map 📋 Mathlib.Algebra.Polynomial.Roots
  (R : Type u) (S : Type v) {T : Type w} [CommRing R] [IsDomain R] [CommRing T] (p : Polynomial T) [CommRing S] [Algebra T S] [Algebra S R] [Algebra T R] [IsScalarTower T S R] : (Polynomial.map (algebraMap T S) p).aroots R = p.aroots R
• Polynomial.eq_rootMultiplicity_map 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) (a : A) : Polynomial.rootMultiplicity a p = Polynomial.rootMultiplicity (f a) (Polynomial.map f p)
• Polynomial.le_rootMultiplicity_map 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {p : Polynomial A} {f : A →+* B} (hmap : Polynomial.map f p ≠ 0) (a : A) : Polynomial.rootMultiplicity a p ≤ Polynomial.rootMultiplicity (f a) (Polynomial.map f p)
• Polynomial.count_map_roots_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] (p : Polynomial A) {f : A →+* B} (hf : Function.Injective ⇑f) (b : B) : Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
• Polynomial.count_map_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] {p : Polynomial A} {f : A →+* B} (hmap : Polynomial.map f p ≠ 0) (b : B) : Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
• Polynomial.map_roots_le_of_injective 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] (p : Polynomial A) {f : A →+* B} (hf : Function.Injective ⇑f) : Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
• Polynomial.map_roots_le 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p ≠ 0) : Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
• Polynomial.roots_map_of_injective_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective ⇑f) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• Polynomial.roots_map_of_map_ne_zero_of_card_eq_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} (f : A →+* B) (h : Polynomial.map f p ≠ 0) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots
• 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.rootSet_maps_to' 📋 Mathlib.Algebra.Polynomial.Roots
  {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} {S' : Type u_2} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] (hp : Polynomial.map (algebraMap T S') p = 0 → Polynomial.map (algebraMap T S) p = 0) (f : S →ₐ[T] S') : Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
• Polynomial.eval_map_algebraMap 📋 Mathlib.RingTheory.Polynomial.Tower
  {R : Type u_1} {B : Type u_3} [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_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
• PolynomialModule.map_smul 📋 Mathlib.Algebra.Polynomial.Module.Basic
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] [Algebra R R'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (p : Polynomial R) (q : PolynomialModule R M) : (PolynomialModule.map R' f) (p • q) = Polynomial.map (algebraMap R R') p • (PolynomialModule.map R' f) q
• Polynomial.mem_lifts 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) : p ∈ Polynomial.lifts f ↔ ∃ q, Polynomial.map f q = p
• Polynomial.lifts_iff_set_range 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) : p ∈ Polynomial.lifts f ↔ p ∈ Set.range (Polynomial.map f)
• Polynomial.mem_lifts_and_degree_eq 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (hlifts : p ∈ Polynomial.lifts f) : ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree
• Polynomial.lifts_and_natDegree_eq_and_monic 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (hlifts : p ∈ Polynomial.lifts f) (hp : p.Monic) : ∃ q, Polynomial.map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
• Polynomial.lifts_and_degree_eq_and_monic 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} [Nontrivial S] {p : Polynomial S} (hlifts : p ∈ Polynomial.lifts f) (hp : p.Monic) : ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree ∧ q.Monic
• Polynomial.mapAlg_eq_map 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (p : Polynomial R) : (Polynomial.mapAlg R S) p = Polynomial.map (algebraMap R S) p
• Polynomial.monomial_mem_lifts_and_degree_eq 📋 Mathlib.Algebra.Polynomial.Lifts
  {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {s : S} {n : ℕ} (hl : (Polynomial.monomial n) s ∈ Polynomial.lifts f) : ∃ q, Polynomial.map f q = (Polynomial.monomial n) s ∧ q.degree = ((Polynomial.monomial n) s).degree
• Polynomial.map_smul 📋 Mathlib.Algebra.Polynomial.Eval.SMul
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (r : R) : Polynomial.map f (r • p) = f r • Polynomial.map f p
• PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = a • Polynomial.map (algebraMap R A) p
• polyEquivTensor_symm_apply_tmul_eq_smul 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = a • Polynomial.map (algebraMap R A) p
• PolyEquivTensor.toFunBilinear_apply_eq_smul 📋 Mathlib.RingTheory.PolynomialAlgebra
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (p : Polynomial R) : ((PolyEquivTensor.toFunBilinear R A) a) p = a • Polynomial.map (algebraMap R A) p
• matPolyEquiv_smul_one 📋 Mathlib.RingTheory.MatrixPolynomialAlgebra
  {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) : matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p
• matPolyEquiv_map_smul 📋 Mathlib.RingTheory.MatrixPolynomialAlgebra
  {R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (p : Polynomial R) (M : Matrix n n (Polynomial R)) : matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M
• Matrix.charpoly_map 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (f : R →+* S) : (M.map ⇑f).charpoly = Polynomial.map f M.charpoly
• Matrix.charmatrix_map 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (f : R →+* S) : (M.map ⇑f).charmatrix = M.charmatrix.map (Polynomial.map f)
• Polynomial.map_scaleRoots 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (p : Polynomial R) (x : R) (f : R →+* S) (h : f p.leadingCoeff ≠ 0) : Polynomial.map f (p.scaleRoots x) = (Polynomial.map f p).scaleRoots (f x)
• IsLocalization.integerNormalization_map_to_map 📋 Mathlib.RingTheory.Localization.Integral
  {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (p : Polynomial S) : ∃ b, Polynomial.map (algebraMap R S) (IsLocalization.integerNormalization M p) = ↑b • p
• Ideal.comap_lt_comap_of_root_mem_sdiff 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I J : Ideal S} [I.IsPrime] (hIJ : I ≤ J) {r : S} (hr : r ∈ ↑J \ ↑I) {p : Polynomial R} (p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0) (hp : Polynomial.eval₂ f r p ∈ I) : Ideal.comap f I < Ideal.comap f J
• Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} {I J : Ideal S} [I.IsPrime] (hIJ : I ≤ J) {r : S} (hr : r ∈ ↑J \ ↑I) {p : Polynomial R} (p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0) (hpI : Polynomial.eval₂ f r p ∈ I) : ∃ i, p.coeff i ∈ ↑(Ideal.comap f J) \ ↑(Ideal.comap f I)
• Ideal.exists_nonzero_mem_of_ne_bot 📋 Mathlib.RingTheory.Ideal.GoingUp
  {R : Type u_1} [CommRing R] {P : Ideal (Polynomial R)} (Pb : P ≠ ⊥) (hP : ∀ (x : R), Polynomial.C x ∈ P → x = 0) : ∃ p ∈ P, Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) p ≠ 0
• Ring.DirectLimit.Polynomial.exists_of 📋 Mathlib.Algebra.Colimit.Ring
  {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i ≤ j → G i →+* G j} [Nonempty ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] (q : Polynomial (Ring.DirectLimit G fun i j h => ⇑(f' i j h))) : ∃ i p, Polynomial.map (Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i) p = q
• Polynomial.monic_map_iff 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [DivisionRing R] [Semiring S] [Nontrivial S] {f : R →+* S} {p : Polynomial R} : (Polynomial.map f p).Monic ↔ p.Monic
• Polynomial.natDegree_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [DivisionRing R] [Semiring S] [Nontrivial S] (p : Polynomial R) (f : R →+* S) : (Polynomial.map f p).degree = p.degree
• Polynomial.leadingCoeff_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.map_ne_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] {f : R →+* S} (hp : p ≠ 0) : Polynomial.map f p ≠ 0
• Polynomial.map_eq_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) : Polynomial.map f p = 0 ↔ p = 0
• Polynomial.isCoprime_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] (f : R →+* k) : IsCoprime (Polynomial.map f p) (Polynomial.map f q) ↔ IsCoprime p q
• Polynomial.isUnit_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [Field k] (f : R →+* k) : IsUnit (Polynomial.map f p) ↔ IsUnit p
• Polynomial.mem_roots_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) : x ∈ (Polynomial.map f p).roots ↔ Polynomial.eval₂ f x p = 0
• Polynomial.map_div 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] (f : R →+* k) : Polynomial.map f (p / q) = Polynomial.map f p / Polynomial.map f q
• Polynomial.map_mod 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] (f : R →+* k) : Polynomial.map f (p % q) = Polynomial.map f p % Polynomial.map f q
• Polynomial.gcd_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] {p q : Polynomial R} [Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) : EuclideanDomain.gcd (Polynomial.map f p) (Polynomial.map f q) = Polynomial.map f (EuclideanDomain.gcd p q)
• Polynomial.map_dvd_map' 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {k : Type y} [Field R] [Field k] (f : R →+* k) {x y : Polynomial R} : Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y
• Polynomial.splits_id_iff_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} : Polynomial.Splits (RingHom.id L) (Polynomial.map i f) ↔ Polynomial.Splits i f
• Polynomial.splits_of_map_degree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : (Polynomial.map i f).degree = 1) : Polynomial.Splits i f
• Polynomial.rootOfSplits' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree ≠ 0) : L
• Polynomial.natDegree_eq_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) : p.natDegree = (Polynomial.map i p).roots.card
• Polynomial.natDegree_eq_card_roots' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) : (Polynomial.map i p).natDegree = (Polynomial.map i p).roots.card
• Polynomial.splits_iff_comp_splits_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : (Polynomial.map i p).degree = 1) : Polynomial.Splits i f ↔ Polynomial.Splits i (f.comp p)
• Polynomial.roots_ne_zero_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : f.natDegree ≠ 0) : (Polynomial.map i f).roots ≠ 0
• Polynomial.Splits.comp_of_map_degree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : (Polynomial.map i p).degree ≤ 1) (h : Polynomial.Splits i f) : Polynomial.Splits i (f.comp p)
• Polynomial.roots_ne_zero_of_splits' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : (Polynomial.map i f).natDegree ≠ 0) : (Polynomial.map i f).roots ≠ 0
• Polynomial.splits_map_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {F : Type u} {K : Type v} {L : Type w} [CommRing K] [Field L] [Field F] (i : K →+* L) (j : L →+* F) {f : Polynomial K} : Polynomial.Splits j (Polynomial.map i f) ↔ Polynomial.Splits (j.comp i) f
• Polynomial.exists_root_of_splits' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : (Polynomial.map i f).degree ≠ 0) : ∃ x, Polynomial.eval₂ i x f = 0
• Polynomial.map_rootOfSplits' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree ≠ 0) : Polynomial.eval₂ i (Polynomial.rootOfSplits' i hf hfd) f = 0
• Polynomial.degree_eq_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : Polynomial.Splits i p) : p.degree = ↑(Polynomial.map i p).roots.card
• Polynomial.splits_id_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (h : Polynomial.Splits i f) (roots_mem_range : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) : Polynomial.Splits (RingHom.id K) f
• Polynomial.roots_map 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits (RingHom.id K) f) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.degree_eq_card_roots' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : Polynomial.map i p ≠ 0) (hsplit : Polynomial.Splits i p) : (Polynomial.map i p).degree = ↑(Polynomial.map i p).roots.card
• Polynomial.splits_of_map_eq_C 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} {a : L} (h : Polynomial.map i f = Polynomial.C a) : Polynomial.Splits i f
• Polynomial.splits_of_splits_mul' 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f g : Polynomial K} (hfg : Polynomial.map i (f * g) ≠ 0) (h : Polynomial.Splits i (f * g)) : Polynomial.Splits i f ∧ Polynomial.Splits i g
• Polynomial.splits_of_comp 📋 Mathlib.Algebra.Polynomial.Splits
  {F : Type u} {K : Type v} {L : Type w} [Field K] [Field L] [Field F] (i : K →+* L) (j : L →+* F) {f : Polynomial K} (h : Polynomial.Splits (j.comp i) f) (roots_mem_range : ∀ a ∈ (Polynomial.map (j.comp i) f).roots, a ∈ j.range) : Polynomial.Splits i f
• Polynomial.rootOfSplits'_eq_rootOfSplits 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : (Polynomial.map i f).degree ≠ 0) : Polynomial.rootOfSplits' i hf hfd = Polynomial.rootOfSplits i hf ⋯
• Polynomial.Splits.def 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] {i : K →+* L} {f : Polynomial K} (h : Polynomial.Splits i f) : f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1
• Polynomial.splits_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) (f : Polynomial K) : Polynomial.Splits i f ↔ f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1
• Polynomial.Splits.eq_1 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (f : Polynomial K) : Polynomial.Splits i f = (Polynomial.map i f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → g.degree = 1)
• Polynomial.eq_X_sub_C_of_splits_of_single_root 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {x : K} {h : Polynomial K} (h_splits : Polynomial.Splits i h) (h_roots : (Polynomial.map i h).roots = {i x}) : h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
• Polynomial.splits_of_exists_multiset 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {s : Multiset L} (hs : Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod) : Polynomial.Splits i f
• Polynomial.splits_iff_exists_multiset 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} : Polynomial.Splits i f ↔ ∃ s, Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod
• Polynomial.eq_prod_roots_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) : Polynomial.map i p = Polynomial.C (i p.leadingCoeff) * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.map i p).roots).prod
• Polynomial.Splits.mem_subfield_of_isRoot 📋 Mathlib.Algebra.Polynomial.Splits
  {K : Type v} [Field K] (F : Subfield K) {f : Polynomial ↥F} (hnz : f ≠ 0) (hf : Polynomial.Splits (RingHom.id ↥F) f) {x : K} (hx : (Polynomial.map F.subtype f).IsRoot x) : x ∈ F
• Cubic.map_toPoly 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} {P : Cubic R} [Semiring R] [Semiring S] {φ : R →+* S} : (Cubic.map φ P).toPoly = Polynomial.map φ P.toPoly
• Cubic.map_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {R : Type u_1} {S : Type u_2} {P : Cubic R} [CommRing R] [CommRing S] {φ : R →+* S} [IsDomain S] : (Cubic.map φ P).roots = (Polynomial.map φ P.toPoly).roots
• Polynomial.generalizedEisenstein 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
  {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] {q f : Polynomial R} {p : ℕ} (hq_irr : Irreducible (Polynomial.map (algebraMap R K) q)) (hq_monic : q.Monic) (hf_prim : f.IsPrimitive) (hfd0 : 0 < f.natDegree) (hfP : (algebraMap R K) f.leadingCoeff ≠ 0) (hfmodP : Polynomial.map (algebraMap R K) f = Polynomial.C ((algebraMap R K) f.leadingCoeff) * Polynomial.map (algebraMap R K) q ^ p) (hfmodP2 : Polynomial.map (Ideal.Quotient.mk (RingHom.ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0) : Irreducible f
• Polynomial.IsWeaklyEisensteinAt.map 📋 Mathlib.RingTheory.Polynomial.Eisenstein.Basic
  {R : Type u} [CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R} (hf : f.IsWeaklyEisensteinAt 𝓟) {A : Type v} [CommSemiring A] (φ : R →+* A) : (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)
• 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.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 (Submodule.span R {p})) : ∃ y ∈ Algebra.adjoin 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 (Submodule.span R {p})) (i : ℕ) : (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ i
• minpoly.map_ne_one 📋 Mathlib.FieldTheory.Minpoly.Basic
  (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Nontrivial B] {R : Type u_4} [Semiring R] [Nontrivial R] (f : A →+* R) : Polynomial.map f (minpoly A x) ≠ 1
• minpoly.dvd_map_of_isScalarTower 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_3) (K : Type u_4) {R : Type u_5} [CommRing A] [Field K] [Ring R] [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) : minpoly K x ∣ Polynomial.map (algebraMap A K) (minpoly A x)
• minpoly.dvd_map_of_isScalarTower' 📋 Mathlib.FieldTheory.Minpoly.Field
  (R : Type u_3) {S : Type u_4} (K : Type u_5) (L : Type u_6) [CommRing R] [CommRing S] [Field K] [Ring L] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S) : minpoly K ((algebraMap S L) s) ∣ Polynomial.map (algebraMap R K) (minpoly R s)
• minpoly.map_algebraMap 📋 Mathlib.FieldTheory.Minpoly.Field
  {F : Type u_3} {E : Type u_4} {A : Type u_5} [Field F] [Field E] [CommRing A] [Algebra F E] [Algebra E A] [Algebra F A] [IsScalarTower F E A] {a : A} (ha : IsIntegral F a) (h : minpoly E a ∈ Polynomial.lifts (algebraMap F E)) : Polynomial.map (algebraMap F E) (minpoly F a) = minpoly E a
• Matrix.charpoly.univ_map_map 📋 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) : Polynomial.map (MvPolynomial.map f) (Matrix.charpoly.univ R n) = Matrix.charpoly.univ S n
• 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
• LinearMap.polyCharpolyAux.eq_1 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) : φ.polyCharpolyAux b bₘ = Polynomial.map (↑(MvPolynomial.bind₁ (LinearMap.toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)
• LinearMap.polyCharpoly_map_eq_charpoly 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (x : L) : Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = LinearMap.charpoly (φ x)
• LinearMap.polyCharpolyAux_map_eq_charpoly 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : L) : Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ x)
• LinearMap.polyCharpoly_eq_of_basis 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) [DecidableEq ιM] (bₘ : Basis ιM R M) : φ.polyCharpoly b = Polynomial.map (↑(MvPolynomial.bind₁ (LinearMap.toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)
• LinearMap.polyCharpolyAux_map_eval 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) [Module.Finite R M] [Module.Free R M] (x : ι → R) : Polynomial.map (MvPolynomial.eval x) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))
• LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (x : L) : Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly
• LinearMap.polyCharpolyAux_baseChange 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (A : Type u_8) [CommRing A] [Algebra R A] : (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpolyAux (Algebra.TensorProduct.basis A b) (Algebra.TensorProduct.basis A bₘ) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b bₘ)
• LinearMap.polyCharpoly_baseChange 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [DecidableEq ι] [Module.Free R M] [Module.Finite R M] (b : Basis ι R L) (A : Type u_8) [CommRing A] [Algebra R A] : (LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpoly (Algebra.TensorProduct.basis A b) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)
• LinearMap.polyCharpolyAux_map_aeval 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
  {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [CommRing R] [AddCommGroup L] [Module R L] [AddCommGroup M] [Module R M] (φ : L →ₗ[R] Module.End R M) [Fintype ι] [Fintype ιM] [DecidableEq ι] [DecidableEq ιM] (b : Basis ι R L) (bₘ : Basis ιM R M) (A : Type u_8) [CommRing A] [Algebra R A] [Module.Finite A (TensorProduct R A M)] [Module.Free A (TensorProduct R A M)] (x : ι → A) : Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) = ((LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ) ((Algebra.TensorProduct.basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly
• LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval 📋 Mathlib.Algebra.Lie.CartanExists
  {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R L] [Module.Free R L] [Module.Finite R M] [Module.Free R M] (x y : L) (r : R) : Polynomial.map (Polynomial.evalRingHom r) (LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y) = LinearMap.charpoly ((LieModule.toEnd R L M) (r • y + x))
• Polynomial.Separable.map 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] {p : Polynomial R} (h : p.Separable) {f : R →+* S} : (Polynomial.map f p).Separable
• Polynomial.separable_map 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {S : Type u_1} [CommRing S] [Nontrivial S] (f : F →+* S) {p : Polynomial F} : (Polynomial.map f p).Separable ↔ p.Separable

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 bce1d65