modByMonic_add_div

Stream: Is there code for X?

[Kenny Lau]

import Mathlib.Algebra.Polynomial.Div

namespace Polynomial

theorem modByMonic_add_div' {R : Type*} [Ring R] (p q : R[X]) : p %ₘ q + q * (p /ₘ q) = p := by
  by_cases hq : q.Monic
  · exact modByMonic_add_div p hq
  · rw [divByMonic_eq_of_not_monic _ hq, modByMonic_eq_of_not_monic _ hq, mul_zero, add_zero]

did we forget to remove the monic assumption?

[Ruben Van de Velde]

Probably! Please pr

[Artie Khovanov]

There's a bunch of lemmas about modByMonic with unnecessary assumptions

[Kenny Lau]

@Ruben Van de Velde @Artie Khovanov #31817 (Artie, would you like to check if I missed any one)