instLinearOrderedCommMonoidWithZero

English

If α is a CommMonoid, LinearOrder α and IsOrderedMonoid α, then WithZero α is LinearOrderedCommMonoidWithZero.

Русский

Если α — коммутативный моноид, линейно упорядочен и упорядочен по умножению, то WithZero α является линейно упорядоченным коммутативным моноидом с нулём.

LaTeX

$$$[CommMonoid\ α] \land [LinearOrder\ α] \land [IsOrderedMonoid\ α] \Rightarrow \mathrm{LinearOrderedCommMonoidWithZero}(\mathrm{WithZero}\ α)$$$

Lean4

instance instLinearOrderedCommMonoidWithZero [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] :
    LinearOrderedCommMonoidWithZero (WithZero α) where zero_le_one := WithZero.zero_le _

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