instLinearOrderedCommGroupWithZero

English

If α is a commutative group, LinearOrder α and IsOrderedMonoid α, then WithZero α is LinearOrderedCommGroupWithZero.

Русский

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

LaTeX

$$$[CommGroup α] \land [LinearOrder α] \land [IsOrderedMonoid α] \Rightarrow \mathrm{LinearOrderedCommGroupWithZero}(\mathrm{WithZero} α)$$$

Lean4

instance instLinearOrderedCommGroupWithZero [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] :
    LinearOrderedCommGroupWithZero (WithZero α) where

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