Documentation

Mathlib.Algebra.Order.GroupWithZero.Synonym

Group with zero structure on the order type synonyms #

Transfer algebraic instances from α to αᵒᵈ and Lex α.

Order dual #

source
@[implicit_reducible]
instance OrderDual.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
MulZeroClass αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] :
MulZeroOneClass αᵒᵈ
source
instance OrderDual.instNoZeroDivisors {α : Type u_1} [Mul α] [Zero α] [NoZeroDivisors α] :
NoZeroDivisors αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] :
SemigroupWithZero αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] :
MonoidWithZero αᵒᵈ
source
instance OrderDual.instIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsLeftCancelMulZero α] :
IsLeftCancelMulZero αᵒᵈ
source
instance OrderDual.instIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsRightCancelMulZero α] :
IsRightCancelMulZero αᵒᵈ
source
instance OrderDual.instIsCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsCancelMulZero α] :
IsCancelMulZero αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommMonoidWithZero {α : Type u_1} [CommMonoidWithZero α] :
CommMonoidWithZero αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
GroupWithZero αᵒᵈ
source
@[implicit_reducible]
instance OrderDual.instCommGroupWithZero {α : Type u_1} [CommGroupWithZero α] :
CommGroupWithZero αᵒᵈ

Lexicographic order #

source
@[implicit_reducible]
instance Lex.instMulZeroClass {α : Type u_1} [MulZeroClass α] :
MulZeroClass (Lex α)
source
@[implicit_reducible]
instance Lex.instMulZeroOneClass {α : Type u_1} [MulZeroOneClass α] :
MulZeroOneClass (Lex α)
source
instance Lex.instNoZeroDivisors {α : Type u_1} [Mul α] [Zero α] [NoZeroDivisors α] :
NoZeroDivisors (Lex α)
source
@[implicit_reducible]
instance Lex.instSemigroupWithZero {α : Type u_1} [SemigroupWithZero α] :
SemigroupWithZero (Lex α)
source
@[implicit_reducible]
instance Lex.instMonoidWithZero {α : Type u_1} [MonoidWithZero α] :
MonoidWithZero (Lex α)
source
instance Lex.instIsLeftCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsLeftCancelMulZero α] :
IsLeftCancelMulZero (Lex α)
source
instance Lex.instIsRightCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsRightCancelMulZero α] :
IsRightCancelMulZero (Lex α)
source
instance Lex.instIsCancelMulZero {α : Type u_1} [Mul α] [Zero α] [IsCancelMulZero α] :
IsCancelMulZero (Lex α)
source
@[implicit_reducible]
instance Lex.instCommMonoidWithZero {α : Type u_1} [CommMonoidWithZero α] :
CommMonoidWithZero (Lex α)
source
@[implicit_reducible]
instance Lex.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
GroupWithZero (Lex α)
source
@[implicit_reducible]
instance Lex.instCommGroupWithZero {α : Type u_1} [CommGroupWithZero α] :
CommGroupWithZero (Lex α)