R : Type u
S : Type ?u.93580
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
⊢ coeff (toSubring p T hp) (natDegree p) = 1 ↔ ↑(coeff (toSubring p T hp) (natDegree p)) = 1
R : Type u
S : Type ?u.93580
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
⊢ Monic (toSubring p T hp) ↔ Monic p
simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]
no goals
R : Type u
S : Type ?u.93580
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
⊢ coeff (toSubring p T hp) (natDegree p) = 1 ↔ ↑(coeff (toSubring p T hp) (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.93580
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
H : coeff (toSubring p T hp) (natDegree p) = 1
⊢ ↑(coeff (toSubring p T hp) (natDegree p)) = 1
rw [H, OneMemClass.coe_one]