instMulZeroClass

Mathlib.Algebra.GroupWithZero.Nat

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

English

0 · x = 0 and x · 0 = 0 for all natural x.

Русский

0 умножение на x равно 0, и x умножение на 0 равно 0 для всех натуральных x.

LaTeX

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

Lean4

instance instMulZeroClass : MulZeroClass ℕ where
  zero_mul := Nat.zero_mul
  mul_zero := Nat.mul_zero

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

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

Разделы

Аффилиация

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