English
Modulo by a monic q is additive: (p1 + p2) mod q = (p1 mod q) + (p2 mod q) when q is monic.
Русский
Остаток по модулю q при делении на моноик аддитивен: (p1 + p2) mod q = (p1 mod q) + (p2 mod q) при q моноик.
LaTeX
$$$ (p_1 + p_2) \bmod q = p_1 \bmod q + p_2 \bmod q $$$
Lean4
theorem add_modByMonic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q :=
by
by_cases hq : q.Monic
· rcases subsingleton_or_nontrivial R with hR | hR
· simp only [eq_iff_true_of_subsingleton]
·
exact
(div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
⟨by
rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc, add_comm (q * _),
modByMonic_add_div _ hq],
(degree_add_le _ _).trans_lt (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2
· simp_rw [modByMonic_eq_of_not_monic _ hq]
