isUnit_of_self_mul_dvd_separable — Mathlib

English

If p is separable and q^2 divides p, then q is a unit.

Русский

Если p разделим и q^2 делит p, то q — единица.

LaTeX

$$$\\operatorname{Separable}(p) \\land q^2 \\mid p \\Rightarrow \\operatorname{IsUnit}(q)$$$

Lean4

theorem isUnit_of_self_mul_dvd_separable {p q : R[X]} (hp : p.Separable) (hq : q * q ∣ p) : IsUnit q :=
  by
  obtain ⟨p, rfl⟩ := hq
  apply isCoprime_self.mp
  have : IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p)) :=
    by
    simp only [← mul_assoc, mul_add]
    dsimp only [Separable] at hp
    convert hp using 1
    rw [derivative_mul, derivative_mul]
    ring
  exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)

Похожие утверждения