Loogle!

Result

Found 579 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.associated_map_map 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {x y : Polynomial R} : Associated x y → Associated (Polynomial.map f x) (Polynomial.map f y)
• 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.eval_map_apply 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : R) : Polynomial.eval (f x) (Polynomial.map f p) = f (Polynomial.eval x p)
• 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.nextCoeff_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).nextCoeff = f p.nextCoeff
• 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.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.mapAlg_eq_map 📋 Mathlib.Algebra.Polynomial.AlgebraMap
  {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.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.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_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).degree = p.degree
• Polynomial.natDegree_map_eq_of_injective 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {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.Degree.Lemmas
  {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.leadingCoeff_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.nextCoeff_map_eq_of_isUnit_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : IsUnit p.leadingCoeff) : (Polynomial.map f p).nextCoeff = f p.nextCoeff
• Polynomial.leadingCoeff_map_of_injective 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {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.Degree.Lemmas
  {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.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.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.MonicDegreeEq.map_coe 📋 Mathlib.Algebra.Polynomial.Monic
  {R : Type u} {S : Type v} {n : ℕ} [Semiring R] [Semiring S] (p : Polynomial.MonicDegreeEq R n) (f : R →+* S) : ↑(p.map f) = Polynomial.map f ↑p
• 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.card_roots_map_le_natDegree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_3} {B : Type u_4} [Semiring A] [CommRing B] [IsDomain B] {f : A →+* B} (p : Polynomial A) : (Polynomial.map f p).roots.card ≤ p.natDegree
• 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.card_roots_map_le_degree 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_3} {B : Type u_4} [Semiring A] [CommRing B] [IsDomain B] {f : A →+* B} (p : Polynomial A) (hp0 : p ≠ 0) : ↑(Polynomial.map f p).roots.card ≤ p.degree
• 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.filter_roots_map_range_eq_map_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {f : A →+* B} [DecidablePred fun x => x ∈ f.range] (hf : Function.Injective ⇑f) (p : Polynomial A) : Multiset.filter (fun x => x ∈ f.range) (Polynomial.map f p).roots = Multiset.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.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
• 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
• 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.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
• 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.monic_map_iff 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Ring R] [IsSimpleRing 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} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (f : R →+* S) : (Polynomial.map f p).natDegree = p.natDegree
• Polynomial.degree_map 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Ring R] [IsSimpleRing 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} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (f : R →+* S) : (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
• Polynomial.nextCoeff_map_eq 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] (p : Polynomial R) (f : R →+* S) : (Polynomial.map f p).nextCoeff = f p.nextCoeff
• Polynomial.map_ne_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} {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} [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p : Polynomial R} (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.map_normalize 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} {S : Type v} [Field R] (p : Polynomial R) [DecidableEq R] [Field S] [DecidableEq S] (f : R →+* S) : Polynomial.map f (normalize p) = normalize (Polynomial.map f p)
• Polynomial.map_taylor 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (p : Polynomial R) (r : R) (f : R →+* S) : Polynomial.map f ((Polynomial.taylor r) p) = (Polynomial.taylor (f r)) (Polynomial.map f p)
• Polynomial.Splits.map 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (Polynomial.map i f).Splits
• Polynomial.Splits.of_algHom 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (e : A →ₐ[R] B) : (Polynomial.map (algebraMap R B) f).Splits
• Polynomial.Splits.of_isScalarTower 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} (B : Type u_3) [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hf : (Polynomial.map (algebraMap R A) f).Splits) : (Polynomial.map (algebraMap R B) f).Splits
• Polynomial.Splits.map_roots 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (i : R →+* S) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.Splits.of_splits_map 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_2} [CommRing S] [IsDomain S] [IsSimpleRing R] (i : R →+* S) (hf : (Polynomial.map i f).Splits) (hi : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) : f.Splits
• Polynomial.Splits.mem_range_of_isRoot 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (hf0 : f ≠ 0) {i : R →+* S} {x : S} (hx : (Polynomial.map i f).IsRoot x) : x ∈ i.range
• Polynomial.Splits.image_rootSet 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [IsSimpleRing A] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : ⇑g '' f.rootSet A = f.rootSet B
• Polynomial.Splits.aeval_eq_prod_aroots_of_monic 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [IsSimpleRing R] [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.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [IsSimpleRing R] [Algebra R A] (hf : (Polynomial.map (algebraMap R A) f).Splits) (x : A) : (Polynomial.aeval x) f = (algebraMap R A) f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) (f.aroots A)).prod
• Polynomial.Splits.adjoin_rootSet_eq_range 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [IsSimpleRing A] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤
• Polynomial.Splits.mem_subfield_of_isRoot 📋 Mathlib.Algebra.Polynomial.Factors
  {R : Type u_1} [Field R] (F : Subfield R) {f : Polynomial ↥F} (hf : f.Splits) (hf0 : f ≠ 0) {x : R} (hx : (Polynomial.map F.subtype f).IsRoot x) : x ∈ 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)
• Polynomial.integralNormalization_map 📋 Mathlib.RingTheory.Polynomial.IntegralNormalization
  {R : Type u} [Semiring R] {A : Type u_1} [Semiring A] (f : R →+* A) (p : Polynomial R) (H : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).integralNormalization = Polynomial.map f p.integralNormalization
• Polynomial.exists_dvd_map_of_isAlgebraic 📋 Mathlib.RingTheory.Algebraic.Integral
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] {f : Polynomial S} (hf : f ≠ 0) : ∃ g, g ≠ 0 ∧ f ∣ Polynomial.map (algebraMap R S) g
• 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 ι] [IsDirectedOrder ι] (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.splits_comp_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (Polynomial.map i f).Splits
• Polynomial.splits_of_splits_id 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (Polynomial.map i f).Splits
• Polynomial.splits_of_algHom 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (e : A →ₐ[R] B) : (Polynomial.map (algebraMap R B) f).Splits
• Polynomial.splits_of_isScalarTower 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} (B : Type u_3) [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hf : (Polynomial.map (algebraMap R A) f).Splits) : (Polynomial.map (algebraMap R B) f).Splits
• 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.map (RingHom.id L) (Polynomial.map i f)).Splits ↔ (Polynomial.map i f).Splits
• Polynomial.roots_map 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (i : R →+* S) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.splits_id_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_2} [CommRing S] [IsDomain S] [IsSimpleRing R] (i : R →+* S) (hf : (Polynomial.map i f).Splits) (hi : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) : f.Splits
• Polynomial.splits_of_comp 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_2} [CommRing S] [IsDomain S] [IsSimpleRing R] (i : R →+* S) (hf : (Polynomial.map i f).Splits) (hi : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) : f.Splits
• Polynomial.splits_map_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {F : Type u} {K : Type v} [CommRing K] [Field F] {L : Type u_2} [CommRing L] (i : K →+* L) (j : L →+* F) {f : Polynomial K} : (Polynomial.map j (Polynomial.map i f)).Splits ↔ (Polynomial.map (j.comp i) f).Splits
• Polynomial.image_rootSet 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [IsSimpleRing A] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : ⇑g '' f.rootSet A = f.rootSet B
• 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.map i f).Splits
• Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [IsSimpleRing R] [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.aeval_eq_prod_aroots_sub_of_splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [IsSimpleRing R] [Algebra R A] (hf : (Polynomial.map (algebraMap R A) f).Splits) (x : A) : (Polynomial.aeval x) f = (algebraMap R A) f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) (f.aroots A)).prod
• Polynomial.adjoin_rootSet_eq_range 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [IsSimpleRing A] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤
• 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.map i f).Splits) (hfd : (Polynomial.map i f).degree ≠ 0) : Polynomial.rootOfSplits hf hfd = Polynomial.rootOfSplits hf ⋯
• 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
• Cubic.splits_iff_card_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) : (Polynomial.map φ P.toPoly).Splits ↔ (Cubic.map φ P).roots.card = 3
• Cubic.splits_iff_roots_eq_three 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) : (Polynomial.map φ P.toPoly).Splits ↔ ∃ x y z, (Cubic.map φ P).roots = {x, y, z}
• Cubic.disc_ne_zero_iff_roots_nodup 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) (hP : (Polynomial.map φ P.toPoly).Splits) : P.discr ≠ 0 ↔ (Cubic.map φ P).roots.Nodup
• Cubic.discr_ne_zero_iff_roots_nodup 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) (hP : (Polynomial.map φ P.toPoly).Splits) : P.discr ≠ 0 ↔ (Cubic.map φ P).roots.Nodup
• Cubic.card_roots_of_disc_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} [DecidableEq K] (ha : P.a ≠ 0) (h3 : (Polynomial.map φ P.toPoly).Splits) (hd : P.discr ≠ 0) : (Cubic.map φ P).roots.toFinset.card = 3
• Cubic.card_roots_of_discr_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} [DecidableEq K] (ha : P.a ≠ 0) (h3 : (Polynomial.map φ P.toPoly).Splits) (hd : P.discr ≠ 0) : (Cubic.map φ P).roots.toFinset.card = 3
• 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

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 6ff4759 serving mathlib revision edaf32c