Additional instances for ordered commutative groups.

ink

def OrderDual.orderedAddCommGroup.proof_2 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : a + b = b + a

Equations

• (_ : ∀ (a b : αᵒᵈ), a + b = b + a) = (_ : ∀ (a b : αᵒᵈ), a + b = b + a)

ink

def OrderDual.orderedAddCommGroup.proof_1 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : αᵒᵈ) : -a + a = 0

Equations

• (_ : ∀ (a : αᵒᵈ), -a + a = 0) = (_ : ∀ (a : αᵒᵈ), -a + a = 0)

ink

def OrderDual.orderedAddCommGroup.proof_3 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)

ink

instance OrderDual.orderedAddCommGroup {α : Type u_1} [inst : OrderedAddCommGroup α] : OrderedAddCommGroup αᵒᵈ

Equations

• OrderDual.orderedAddCommGroup = let src := OrderDual.orderedAddCommMonoid; let src_1 := instAddGroupOrderDual; OrderedAddCommGroup.mk (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)

ink

instance OrderDual.orderedCommGroup {α : Type u_1} [inst : OrderedCommGroup α] : OrderedCommGroup αᵒᵈ

Equations

• OrderDual.orderedCommGroup = let src := OrderDual.orderedCommMonoid; let src_1 := instGroupOrderDual; OrderedCommGroup.mk (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c * a ≤ c * b)

ink

def OrderDual.linearOrderedAddCommGroup.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)

ink

def OrderDual.linearOrderedAddCommGroup.proof_3 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : min a b = if a ≤ b then a else b

Equations

• (_ : ∀ (a b : αᵒᵈ), min a b = if a ≤ b then a else b) = (_ : ∀ (a b : αᵒᵈ), min a b = if a ≤ b then a else b)

ink

def OrderDual.linearOrderedAddCommGroup.proof_4 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : max a b = if a ≤ b then b else a

Equations

• (_ : ∀ (a b : αᵒᵈ), max a b = if a ≤ b then b else a) = (_ : ∀ (a b : αᵒᵈ), max a b = if a ≤ b then b else a)

ink

instance OrderDual.linearOrderedAddCommGroup {α : Type u_1} [inst : LinearOrderedAddCommGroup α] : LinearOrderedAddCommGroup αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderDual.linearOrderedAddCommGroup.proof_2 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b ∨ b ≤ a

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a) = (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a)

ink

instance OrderDual.linearOrderedCommGroup {α : Type u_1} [inst : LinearOrderedCommGroup α] : LinearOrderedCommGroup αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.