dvd_C_mul — Mathlib

English

If a ≠ 0, then C(a) · p divides q if and only if p divides q.

Русский

Если a ≠ 0, то C(a) · p делит q тогда и только тогда, когда p делит q.

LaTeX

$$ (ha : a ≠ 0) : C a * p ∣ q ↔ p ∣ q$$

Lean4

theorem dvd_C_mul (ha : a ≠ 0) : p ∣ Polynomial.C a * q ↔ p ∣ q :=
  ⟨fun ⟨r, hr⟩ =>
    ⟨C a⁻¹ * r, by rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one, one_mul]⟩,
    fun h => dvd_trans h (dvd_mul_left _ _)⟩

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