case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
⊢ c • p %ₘ q = c • (p %ₘ q)

case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : ¬Monic q
⊢ c • p %ₘ q = c • (p %ₘ q)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
⊢ c • p %ₘ q = c • (p %ₘ q)
by_cases hq : q.Monic
case pos.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)

case pos.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
⊢ c • p %ₘ q = c • (p %ₘ q)
cases' subsingleton_or_nontrivial R with hR hR
no goals
case pos.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)
simp only [eq_iff_true_of_subsingleton]
no goals
case pos.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)
exact
(div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
    ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq],
      (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : Monic q
hR : Nontrivial R
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p
rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq]
no goals
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q : R[X]
inst✝ : Semiring S
c : R
p : R[X]
hq : ¬Monic q
⊢ c • p %ₘ q = c • (p %ₘ q)
simp_rw [modByMonic_eq_of_not_monic _ hq]