monic_of_isUnit_leadingCoeff_inv_smul

English

If the leading coefficient of p is a unit in R, then the scaled polynomial h⁻¹ · p is monic, where h is a witness that p.leadingCoeff is a unit.

Русский

Если ведущий коэффициент p является единицей, то (h⁻¹) · p монична, где h — свидетельство того, что p.leadingCoeff — единица.

LaTeX

$$$\forall p\, (\text{IsUnit}(p_{\operatorname{leadingCoeff}}) \Rightarrow \operatorname{Monic}\left(p_{\operatorname{leadingCoeff}}^{-1} \cdot p\right)).$$$

Lean4

theorem monic_of_isUnit_leadingCoeff_inv_smul (h : IsUnit p.leadingCoeff) : Monic (h.unit⁻¹ • p) :=
  by
  rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
  simp

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