div_C_mul — Mathlib

English

For any polynomials p and q over a field, dividing by C(a) is the same as multiplying by C(a)⁻¹ on the right: p / (C(a) · q) = C(a)⁻¹ · (p / q) when a ≠ 0.

Русский

Любой полином делится на константу C(a) через умножение на C(a)⁻¹: p / (C(a) · q) = C(a)⁻¹ · (p / q) при a ≠ 0.

LaTeX

$$hq : a ≠ 0 → p / (C a * q) = C a⁻¹ * (p / q)$$

Lean4

theorem div_C_mul : p / (C a * q) = C a⁻¹ * (p / q) :=
  by
  by_cases ha : a = 0
  · simp [ha]
  simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]
  congr 3
  rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]

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