monic_zero_iff_subsingleton

Mathlib.Algebra.Polynomial.Monic

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

English

In a semiring R, the zero polynomial is monic if and only if R is a subsingleton.

Русский

В полупрямой системе R нулевой многочлен является моничным тогда и только тогда, когда R — subsingleton.

LaTeX

$$$\operatorname{Monic}(0) \iff \operatorname{Subsingleton}(R).$$$

Lean4

theorem monic_zero_iff_subsingleton : Monic (0 : R[X]) ↔ Subsingleton R :=
  subsingleton_iff_zero_eq_one

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

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

Разделы

Аффилиация

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