Additional instances for ordered commutative groups. #
theorem
OrderDual.orderedAddCommGroup.proof_4
{α : Type u_1}
[OrderedAddCommGroup α]
(n : ℕ)
(a : αᵒᵈ)
:
SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
theorem
OrderDual.orderedAddCommGroup.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.orderedAddCommGroup.proof_3
{α : Type u_1}
[OrderedAddCommGroup α]
(n : ℕ)
(a : αᵒᵈ)
:
SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
Equations
- OrderDual.orderedAddCommGroup = let __src := OrderDual.orderedAddCommMonoid; let __src_1 := OrderDual.instAddGroup; OrderedAddCommGroup.mk ⋯
theorem
OrderDual.orderedAddCommGroup.proof_2
{α : Type u_1}
[OrderedAddCommGroup α]
(a : αᵒᵈ)
:
SubNegMonoid.zsmul 0 a = 0
theorem
OrderDual.orderedAddCommGroup.proof_6
{α : Type u_1}
[OrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- OrderDual.orderedCommGroup = let __src := OrderDual.orderedCommMonoid; let __src_1 := OrderDual.instGroup; OrderedCommGroup.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderDual.linearOrderedAddCommGroup.proof_3
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCommGroup.proof_4
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
compare a b = compareOfLessAndEq a b
theorem
OrderDual.linearOrderedAddCommGroup.proof_2
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCommGroup.proof_1
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- One or more equations did not get rendered due to their size.