irreducible_mul_leadingCoeff_inv — Mathlib

English

For a nonzero polynomial p over a division ring, p is irreducible if and only if p multiplied by the inverse of its leading coefficient is irreducible.

Русский

Для ненулевого многочлена p над кольцом делений: p ирредукционный тогда и только тогда, когда p·(leadingCoeff(p))^{-1} ирредукционный.

LaTeX

$$$p \\neq 0 \\Rightarrow \\bigl( \\operatorname{Irreducible}(p \\cdot C(\\operatorname{leadingCoeff}(p))^{-1}) \\iff \\operatorname{Irreducible}(p) \\bigr)$$$

Lean4

@[simp]
theorem irreducible_mul_leadingCoeff_inv {p : K[X]} : Irreducible (p * C (leadingCoeff p)⁻¹) ↔ Irreducible p :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  exact irreducible_mul_isUnit (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))

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