sub_modByMonic

Mathlib.Algebra.Polynomial.Div

URI: https://scilib.ai/kg/mathlib#Polynomial.sub_modByMonic

English

Subtraction coheres with modulo by a monic: (p1 − p2) mod q = (p1 mod q) − (p2 mod q).

Русский

Вычитание совместимо с модулем по моноику: (p1 − p2) mod q = (p1 mod q) − (p2 mod q).

LaTeX

$$$ (p_1 - p_2) \bmod q = p_1 \bmod q - p_2 \bmod q $$$

Lean4

theorem sub_modByMonic (p₁ p₂ q : R[X]) : (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q := by
  simp [sub_eq_add_neg, add_modByMonic, neg_modByMonic]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru