Documentation

Mathlib.Algebra.Order.Group.Instances

Additional instances for ordered commutative groups. #

def OrderDual.orderedAddCommGroup.proof_2 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
a + b = b + a
Equations
def OrderDual.orderedAddCommGroup.proof_1 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : αᵒᵈ) :
-a + a = 0
Equations
def OrderDual.orderedAddCommGroup.proof_3 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
Equations
Equations
Equations
def OrderDual.linearOrderedAddCommGroup.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
Equations
def OrderDual.linearOrderedAddCommGroup.proof_3 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a b then a else b
Equations
def OrderDual.linearOrderedAddCommGroup.proof_4 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a b then b else a
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.