leadingCoeff_div — Mathlib

English

If q ≠ 0 and deg q ≤ deg p, then the leading coefficient of p/q equals the leading coefficient of p divided by the leading coefficient of q.

Русский

Если q ≠ 0 и deg q ≤ deg p, то leadingCoeff(p/q) = leadingCoeff(p) / leadingCoeff(q).

LaTeX

$$hq : q ≠ 0 → (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff$$

Lean4

theorem leadingCoeff_div (hpq : q.degree ≤ p.degree) : (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff :=
  by
  by_cases hq : q = 0
  · simp [hq]
  rw [div_def, leadingCoeff_mul, leadingCoeff_C, leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _,
    mul_comm, div_eq_mul_inv]
  rwa [degree_mul_leadingCoeff_inv q hq]

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