monic_of_degree_le — Mathlib

English

If b ∈ R satisfies b · p.leadingCoeff = 1, then p · C b is monic.

Русский

Пусть b ∈ R и b · p.leadingCoeff = 1; тогда p · C b моничен.

LaTeX

$$$\text{If } b \in R \text{ with } b \cdot p.leadingCoeff = 1,\; (p \cdot C b)\text{ Monic}.$$$

Lean4

theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : Monic p :=
  Decidable.byCases (fun H : degree p < n => eq_of_zero_eq_one (H2 ▸ (coeff_eq_zero_of_degree_lt H).symm) _ _)
    fun H : ¬degree p < n => by rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]

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