isPrimal_zero

Mathlib.Algebra.GroupWithZero.Divisibility

URI: https://scilib.ai/kg/mathlib#isPrimal_zero

English

Zero is a primal element in a MonoidWithZero.

Русский

Ноль является примальным элементом в MonoidWithZero.

LaTeX

$$IsPrimal(0)$$

Lean4

theorem isPrimal_zero : IsPrimal (0 : α) := fun a b h ↦ ⟨a, b, dvd_rfl, dvd_rfl, (zero_dvd_iff.mp h).symm⟩

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

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

Разделы

Аффилиация

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