int_monic_iff

Mathlib.Algebra.Ring.Subring.IntPolynomial

URI: https://scilib.ai/kg/mathlib#Polynomial.int_monic_iff

English

P.int R hP is monic if and only if P is monic.

Русский

Полином P.int R hP моноичен тогда и только тогда, когда P моноичен.

LaTeX

$$$ (P.int R hP).Monic \iff P.Monic$$$

Lean4

@[simp]
theorem int_monic_iff : (P.int R hP).Monic ↔ P.Monic := by
  rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru