Additional instances for ordered commutative groups. #
Equations
- (_ : ∀ (a b : αᵒᵈ), a + b = b + a) = (_ : ∀ (a b : αᵒᵈ), a + b = b + a)
Equations
- (_ : ∀ (a : αᵒᵈ), -a + a = 0) = (_ : ∀ (a : αᵒᵈ), -a + a = 0)
Equations
- (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)
Equations
- OrderDual.orderedAddCommGroup = let src := OrderDual.orderedAddCommMonoid;
let src_1 := instAddGroupOrderDual;
OrderedAddCommGroup.mk (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)
Equations
- OrderDual.orderedCommGroup = let src := OrderDual.orderedCommMonoid;
let src_1 := instGroupOrderDual;
OrderedCommGroup.mk (_ : ∀ (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)
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)
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)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a) = (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a)
Equations
- One or more equations did not get rendered due to their size.