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 (↑n.succ) a
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
Equations
- OrderDual.orderedAddCommGroup = let __src := OrderDual.orderedAddCommMonoid; let __src_1 := OrderDual.instAddGroup; OrderedAddCommGroup.mk ⋯
theorem
OrderDual.orderedAddCommGroup.proof_6
{α : Type u_1}
[OrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.orderedAddCommGroup.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.orderedAddCommGroup.proof_2
{α : Type u_1}
[OrderedAddCommGroup α]
(a : αᵒᵈ)
:
SubNegMonoid.zsmul 0 a = 0
Equations
- OrderDual.orderedCommGroup = let __src := OrderDual.orderedCommMonoid; let __src_1 := OrderDual.instGroup; OrderedCommGroup.mk ⋯
theorem
OrderDual.linearOrderedAddCommGroup.proof_1
{α : 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_3
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderDual.linearOrderedAddCommGroup.proof_2
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- One or more equations did not get rendered due to their size.