R : Type u
S : Type ?u.75263
inst✝ : Ring R
p : R[X]
⊢ coeff (restriction p) (natDegree p) = 1 ↔ coeff p (natDegree p) = 1
R : Type u
S : Type ?u.75263
inst✝ : Ring R
p : R[X]
⊢ Monic (restriction p) ↔ Monic p
simp only [Monic, leadingCoeff, natDegree_restriction]
R : Type u
S : Type ?u.75263
inst✝ : Ring R
p : R[X]
⊢ coeff (restriction p) (natDegree p) = 1 ↔ ↑(coeff (restriction p) (natDegree p)) = 1
R : Type u
S : Type ?u.75263
inst✝ : Ring R
p : R[X]
⊢ coeff (restriction p) (natDegree p) = 1 ↔ coeff p (natDegree p) = 1
rw [← @coeff_restriction _ _ p]
no goals
R : Type u
S : Type ?u.75263
inst✝ : Ring R
p : R[X]
⊢ coeff (restriction p) (natDegree p) = 1 ↔ ↑(coeff (restriction p) (natDegree p)) = 1
exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩
no goals
R : Type u
S : Type ?u.75263
inst✝ : Ring R
p : R[X]
H : coeff (restriction p) (natDegree p) = 1
⊢ ↑(coeff (restriction p) (natDegree p)) = 1
rw [H, OneMemClass.coe_one]