mul_div_eq_iff_isRoot — Mathlib

English

If q is monic, then p /ₘ q equals p / q, i.e., division by a monic polynomial is identical to ordinary polynomial division.

Русский

Если q монический, то p /ₘ q равняется p / q, то есть деление по монике совпадает с обычным делением.

LaTeX

$$$ p /_{\mathrm{monic}}\; q = p / q \quad (\text{при } q \text{ монический})$$$

Lean4

theorem mul_div_eq_iff_isRoot : (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a :=
  divByMonic_eq_div p (monic_X_sub_C a) ▸ mul_divByMonic_eq_iff_isRoot

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