Documentation

Mathlib.Algebra.Order.GroupWithZero.Synonym

Group with zero structure on the order type synonyms #

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

Order dual #

instance instMulZeroClassOrderDual {α : Type u_1} [h : MulZeroClass α] :

MulZeroClass αᵒᵈ

Equations

instance instMulZeroOneClassOrderDual {α : Type u_1} [h : MulZeroOneClass α] :

MulZeroOneClass αᵒᵈ

Equations

instance instNoZeroDivisorsOrderDual {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] :

NoZeroDivisors αᵒᵈ

instance instSemigroupWithZeroOrderDual {α : Type u_1} [h : SemigroupWithZero α] :

SemigroupWithZero αᵒᵈ

Equations

instance instMonoidWithZeroOrderDual {α : Type u_1} [h : MonoidWithZero α] :

MonoidWithZero αᵒᵈ

Equations

instance instIsLeftCancelMulZeroOrderDual {α : Type u_1} [Mul α] [Zero α] [h : IsLeftCancelMulZero α] :

IsLeftCancelMulZero αᵒᵈ

instance instIsRightCancelMulZeroOrderDual {α : Type u_1} [Mul α] [Zero α] [h : IsRightCancelMulZero α] :

IsRightCancelMulZero αᵒᵈ

instance instIsCancelMulZeroOrderDual {α : Type u_1} [Mul α] [Zero α] [h : IsCancelMulZero α] :

IsCancelMulZero αᵒᵈ

instance instCommMonoidWithZeroOrderDual {α : Type u_1} [h : CommMonoidWithZero α] :

CommMonoidWithZero αᵒᵈ

Equations

instance instGroupWithZeroOrderDual {α : Type u_1} [h : GroupWithZero α] :

GroupWithZero αᵒᵈ

Equations

instance instCommGroupWithZeroOrderDual {α : Type u_1} [h : CommGroupWithZero α] :

CommGroupWithZero αᵒᵈ

Equations

Lexicographic order #

instance instMulZeroClassLex {α : Type u_1} [h : MulZeroClass α] :

MulZeroClass (Lex α)

Equations

instance instMulZeroOneClassLex {α : Type u_1} [h : MulZeroOneClass α] :

MulZeroOneClass (Lex α)

Equations

instance instNoZeroDivisorsLex {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] :

NoZeroDivisors (Lex α)

instance instSemigroupWithZeroLex {α : Type u_1} [h : SemigroupWithZero α] :

SemigroupWithZero (Lex α)

Equations

instance instMonoidWithZeroLex {α : Type u_1} [h : MonoidWithZero α] :

MonoidWithZero (Lex α)

Equations

instance instIsLeftCancelMulZeroLex {α : Type u_1} [Mul α] [Zero α] [h : IsLeftCancelMulZero α] :

IsLeftCancelMulZero (Lex α)

instance instIsRightCancelMulZeroLex {α : Type u_1} [Mul α] [Zero α] [h : IsRightCancelMulZero α] :

IsRightCancelMulZero (Lex α)

instance instIsCancelMulZeroLex {α : Type u_1} [Mul α] [Zero α] [h : IsCancelMulZero α] :

IsCancelMulZero (Lex α)

instance instCommMonoidWithZeroLex {α : Type u_1} [h : CommMonoidWithZero α] :

CommMonoidWithZero (Lex α)

Equations

instance instGroupWithZeroLex {α : Type u_1} [h : GroupWithZero α] :

GroupWithZero (Lex α)

Equations

instance instCommGroupWithZeroLex {α : Type u_1} [h : CommGroupWithZero α] :

CommGroupWithZero (Lex α)

Equations