Additional instances for ordered commutative groups.

theorem OrderDual.orderedAddCommGroup.proof_3 {α : Type u_1} [OrderedAddCommGroup α] (n : ℕ) (a : αᵒᵈ) : SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a

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

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

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

theorem OrderDual.orderedAddCommGroup.proof_2 {α : Type u_1} [OrderedAddCommGroup α] (a : αᵒᵈ) : SubNegMonoid.zsmul 0 a = 0

theorem OrderDual.orderedAddCommGroup.proof_4 {α : Type u_1} [OrderedAddCommGroup α] (n : ℕ) (a : αᵒᵈ) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a

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

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

Equations

• OrderDual.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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

Equations

• OrderDual.orderedCommGroup = OrderedCommGroup.mk ⋯

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

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

Equations

• OrderDual.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

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

theorem OrderDual.linearOrderedAddCommGroup.proof_4 {α : Type u_1} [LinearOrderedAddCommGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : compare a b = compareOfLessAndEq a b

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

Equations

• OrderDual.linearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯