instMulZeroOneClass

Mathlib.Algebra.GroupWithZero.Nat

URI: https://scilib.ai/kg/mathlib#Nat.instMulZeroOneClass

English

Nat has a zero and a one with standard multiplication behavior.

Русский

У натуральных чисел есть ноль и единица с обычной умножением.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{N}, 0 \\cdot x = 0 \\land x \\cdot 0 = 0$$$

Lean4

instance instMulZeroOneClass : MulZeroOneClass ℕ
    where
  __ := instMulZeroClass
  __ := instMulOneClass

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

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

Разделы

Аффилиация

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