R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
f : AdjoinRoot g
⊢ ↑(mk g) (↑(modByMonicHom hg) f) = f
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
⊢ Function.LeftInverse ↑(mk g) ↑(modByMonicHom hg)
intro f
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ ↑(mk g) (↑(modByMonicHom hg) (↑(mk g) p✝)) = ↑(mk g) p✝
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
f : AdjoinRoot g
⊢ ↑(mk g) (↑(modByMonicHom hg) f) = f
induction f using AdjoinRoot.induction_on
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ g ∣ g * (p✝ /ₘ g)
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ ↑(mk g) (↑(modByMonicHom hg) (↑(mk g) p✝)) = ↑(mk g) p✝
rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel_left,
  dvd_neg]
no goals
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ g ∣ g * (p✝ /ₘ g)
apply dvd_mul_right