monic_toSubring — Mathlib

English

The toSubring construction preserves monicity: p is monic iff its toSubring is monic.

Русский

Конструкция toSubring сохраняет моничность: p моничный тогда и только тогда, когда его toSubring моничен.

LaTeX

$$$\\mathrm{Monic}(\\mathrm{toSubring}\\ p\\ T\\ hp) \\;\\Leftrightarrow\\; \\mathrm{Monic}(p)$$$

Lean4

@[simp]
theorem monic_toSubring : Monic (toSubring p T hp) ↔ Monic p :=
  by
  simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]
  exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

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