R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ ↑(IsUnit.unit h)⁻¹ • leadingCoeff p = 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ Monic ((IsUnit.unit h)⁻¹ • p)
rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ ↑(IsUnit.unit (_ : ∃ u, ↑u = leadingCoeff p))⁻¹ • leadingCoeff p = 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ ↑(IsUnit.unit h)⁻¹ • leadingCoeff p = 1
obtain ⟨k, hk⟩ := h
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ k = IsUnit.unit (_ : IsUnit ↑k) * 1
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ ↑(IsUnit.unit (_ : ∃ u, ↑u = leadingCoeff p))⁻¹ • leadingCoeff p = 1
simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]
no goals
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ k = IsUnit.unit (_ : IsUnit ↑k) * 1
simp [Units.ext_iff, IsUnit.unit_spec]