instLinearOrderedCommMonoidWithZero

English

The natural numbers form a LinearOrderedCommMonoidWithZero.

Русский

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

LaTeX

$$LinearOrderedCommMonoidWithZero $\\mathbb{N}$$$

Lean4

instance instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ
    where
  bot := 0
  bot_le := zero_le
  zero_le_one := zero_le_one
  mul_le_mul_left _ _ h c := Nat.mul_le_mul_left c h

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