theorem SomeLocalRings.derivative_nonroot_on_roots_of_irreducible_of_natDegree_lt {𝕜 : Type u_1} [Field 𝕜] (P Q : Polynomial 𝕜) (hP : Irreducible P) (hdeg : Q.natDegree < P.natDegree) (hQ' : Polynomial.derivative Q ≠ 0) (α : AlgebraicClosure 𝕜) : (Polynomial.map (algebraMap 𝕜 (AlgebraicClosure 𝕜)) P).IsRoot α → ¬(Polynomial.map (algebraMap 𝕜 (AlgebraicClosure 𝕜)) (Polynomial.derivative Q)).IsRoot α

If P is irreducible and Q has smaller degree, then a nonzero Q' has no roots among the roots of P in an algebraic closure.

theorem SomeLocalRings.proposition_2_7 {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f.toRingHom σ_f) (σX : Polynomial 𝕜 ≃+* Polynomial 𝕜) (hσX : σX Polynomial.X = Polynomial.X ∧ RingHom.StabilizesBaseFieldWith σX.toRingHom σ_f) (Qf Sf : Polynomial 𝕜) (hQfdeg : Qf.natDegree < P₁.natDegree) (hSf : (σX P₁).comp Qf = Sf * P₂) : IsCoprime Sf P₂ ↔ Polynomial.derivative Qf ≠ 0

Proposition 2.7 Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. Let f : 𝕜[X]/(P₁) ≃+* 𝕜[X]/(P₂) be a ring isomorphism stabilizing 𝕜. Let S_f be as in Proposition 2.4, so that (σ_f^X(P₁)) ∘ Q_f = S_f * P₂ for some Q_f ∈ 𝕜[X]. Then S_f is coprime to P₂ if and only if the formal derivative Q_f' is nonzero.

theorem SomeLocalRings.stabilizesBaseFieldWith_quotientMap_pow {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (n : ℕ) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (σ_f : 𝕜 ≃+* 𝕜) (hfX : RingHom.StabilizesBaseFieldWith fX σ_f) (hIJn : Ideal.span {P₁ ^ n} ≤ Ideal.comap fX (Ideal.span {P₂ ^ n})) : RingHom.StabilizesBaseFieldWith (Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn) σ_f

If a ring homomorphism fX : 𝕜[X] → 𝕜[X] stabilizes the base field via σ_f, then the induced quotient map 𝕜[X]/(P₁^n) → 𝕜[X]/(P₂^n) also stabilizes the base field via σ_f.