monic_scaleRoots_iff — Mathlib

English

scaleRoots(p, s) is monic if and only if p is monic.

Русский

scaleRoots(p, s) моноцикличен тогда и только тогда, когда p моноцикличен.

LaTeX

$$$\operatorname{Monic}(\operatorname{scaleRoots}(p, s)) \;\Leftrightarrow\; \operatorname{Monic}(p)$$$

Lean4

theorem monic_scaleRoots_iff {p : R[X]} (s : R) : Monic (scaleRoots p s) ↔ Monic p := by
  simp only [Monic, leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]

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