divByMonic_eq_div — Mathlib

English

If q is monic, then the monic division of p by q equals the ordinary division: p /ₘ q = p / q.

Русский

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

LaTeX

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

Lean4

theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
  show p /ₘ q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹)) by
    simp only [Monic.def.1 hq, inv_one, C_1, one_mul, mul_one]

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