rw [Polynomial.dvd_iff_modByMonic_eq_zero]
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ (t * p).modByMonic t = 0
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic