monic_restriction — Mathlib

English

A polynomial is monic after restriction if and only if it was monic before restriction.

Русский

Полином моничный после ограничения тогда и только тогда, когда он был моничный до ограничения.

LaTeX

$$$\\mathrm{Monic}(\\mathrm{restriction}(p)) \\;\\Leftrightarrow\\; \\mathrm{Monic}(p)$$$

Lean4

@[simp]
theorem monic_restriction {p : R[X]} : Monic (restriction p) ↔ Monic p :=
  by
  simp only [Monic, leadingCoeff, natDegree_restriction]
  rw [← @coeff_restriction _ _ p]
  exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

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