monic_of_a_eq_one — Mathlib

English

If a cubic P over a semiring R has its leading coefficient a equal to 1, then P.toPoly is Monic.

Русский

Если кубический многочлен P над полем/кольцом R имеет ведущий коэффициент a, равный 1, то P.toPoly монический.

LaTeX

$$$P.a = 1 \\Rightarrow P.toPoly.Monic$$$

Lean4

theorem monic_of_a_eq_one (ha : P.a = 1) : P.toPoly.Monic :=
  by
  nontriviality R
  rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]

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