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
instance instMulZeroClassOrderDual {α : Type u_1} [h : MulZeroClass α] :
MulZeroClass αᵒᵈ
Equations
  • instMulZeroClassOrderDual = h
source
instance instMulZeroOneClassOrderDual {α : Type u_1} [h : MulZeroOneClass α] :
MulZeroOneClass αᵒᵈ
Equations
  • instMulZeroOneClassOrderDual = h
source
theorem instNoZeroDivisorsOrderDual {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] :
NoZeroDivisors αᵒᵈ
source
instance instSemigroupWithZeroOrderDual {α : Type u_1} [h : SemigroupWithZero α] :
SemigroupWithZero αᵒᵈ
Equations
  • instSemigroupWithZeroOrderDual = h
source
instance instMonoidWithZeroOrderDual {α : Type u_1} [h : MonoidWithZero α] :
MonoidWithZero αᵒᵈ
Equations
  • instMonoidWithZeroOrderDual = h
source
instance instCancelMonoidWithZeroOrderDual {α : Type u_1} [h : CancelMonoidWithZero α] :
CancelMonoidWithZero αᵒᵈ
Equations
  • instCancelMonoidWithZeroOrderDual = h
source
instance instCommMonoidWithZeroOrderDual {α : Type u_1} [h : CommMonoidWithZero α] :
CommMonoidWithZero αᵒᵈ
Equations
  • instCommMonoidWithZeroOrderDual = h
source
instance instCancelCommMonoidWithZeroOrderDual {α : Type u_1} [h : CancelCommMonoidWithZero α] :
CancelCommMonoidWithZero αᵒᵈ
Equations
  • instCancelCommMonoidWithZeroOrderDual = h
source
instance instGroupWithZeroOrderDual {α : Type u_1} [h : GroupWithZero α] :
GroupWithZero αᵒᵈ
Equations
  • instGroupWithZeroOrderDual = h
source
instance instCommGroupWithZeroOrderDual {α : Type u_1} [h : CommGroupWithZero α] :
CommGroupWithZero αᵒᵈ
Equations
  • instCommGroupWithZeroOrderDual = h

Lexicographic order #

source
instance instMulZeroClassLex {α : Type u_1} [h : MulZeroClass α] :
MulZeroClass (Lex α)
Equations
  • instMulZeroClassLex = h
source
instance instMulZeroOneClassLex {α : Type u_1} [h : MulZeroOneClass α] :
MulZeroOneClass (Lex α)
Equations
  • instMulZeroOneClassLex = h
source
theorem instNoZeroDivisorsLex {α : Type u_1} [Mul α] [Zero α] [h : NoZeroDivisors α] :
NoZeroDivisors (Lex α)
source
instance instSemigroupWithZeroLex {α : Type u_1} [h : SemigroupWithZero α] :
SemigroupWithZero (Lex α)
Equations
  • instSemigroupWithZeroLex = h
source
instance instMonoidWithZeroLex {α : Type u_1} [h : MonoidWithZero α] :
MonoidWithZero (Lex α)
Equations
  • instMonoidWithZeroLex = h
source
instance instCancelMonoidWithZeroLex {α : Type u_1} [h : CancelMonoidWithZero α] :
CancelMonoidWithZero (Lex α)
Equations
  • instCancelMonoidWithZeroLex = h
source
instance instCommMonoidWithZeroLex {α : Type u_1} [h : CommMonoidWithZero α] :
CommMonoidWithZero (Lex α)
Equations
  • instCommMonoidWithZeroLex = h
source
instance instCancelCommMonoidWithZeroLex {α : Type u_1} [h : CancelCommMonoidWithZero α] :
CancelCommMonoidWithZero (Lex α)
Equations
  • instCancelCommMonoidWithZeroLex = h
source
instance instGroupWithZeroLex {α : Type u_1} [h : GroupWithZero α] :
GroupWithZero (Lex α)
Equations
  • instGroupWithZeroLex = h
source
instance instCommGroupWithZeroLex {α : Type u_1} [h : CommGroupWithZero α] :
CommGroupWithZero (Lex α)
Equations
  • instCommGroupWithZeroLex = h