monic_of_monic_mapAlg — Mathlib

English

If mapAlg R S applied to p is monic, then p is monic (assuming faithful scalar action).

Русский

Если mapAlg R S применён к p и получился моничный полином, то p также моничен (при достоверности скаляра).

LaTeX

$$$ (\mathrm{mapAlg}\, R\, S\ p).Monic \Rightarrow p.Monic $$$

Lean4

theorem monic_of_monic_mapAlg [FaithfulSMul R S] {p : Polynomial R} (hp : (mapAlg R S p).Monic) : p.Monic :=
  monic_of_injective (FaithfulSMul.algebraMap_injective R S) hp

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