monic_of_injective — Mathlib

English

If f is injective and (p.map f) is monic, then p is monic.

Русский

Если f инъективен и (p.map f) мононичен, то p мононичен.

LaTeX

$$$\forall {R} {S} [\text{Semiring } R] [\text{Semiring } S] {f : R \rightarrow+* S} (hf : Injective f) {p : R[X]}, (p.map f).Monic \rightarrow p.Monic$$$

Lean4

theorem monic_of_injective (hf : Injective f) {p : R[X]} (hp : (p.map f).Monic) : p.Monic :=
  by
  apply hf
  rw [← leadingCoeff_of_injective hf, hp.leadingCoeff, f.map_one]

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