The units of an ordered commutative monoid form an ordered commutative group

instance Units.orderedCommGroup {α : Type u_1} [OrderedCommMonoid α] : OrderedCommGroup αˣ

The units of an ordered commutative monoid form an ordered commutative group.

Equations

• Units.orderedCommGroup = OrderedCommGroup.mk ⋯

theorem AddUnits.orderedAddCommGroup.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] : ∀ (x x_1 : AddUnits α), x ≤ x_1 → ∀ (x_2 : AddUnits α), ↑x_2 + ↑x ≤ ↑x_2 + ↑x_1

instance AddUnits.orderedAddCommGroup {α : Type u_1} [OrderedAddCommMonoid α] : OrderedAddCommGroup (AddUnits α)

The units of an ordered commutative additive monoid form an ordered commutative additive group.

Equations

• AddUnits.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

instance Units.instLinearOrderedCommGroup {α : Type u_1} [LinearOrderedCommMonoid α] : LinearOrderedCommGroup αˣ

The units of a linearly ordered commutative monoid form a linearly ordered commutative group.

Equations

• Units.instLinearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

theorem AddUnits.instLinearOrderedAddCommGroup.proof_2 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : a ≤ b ∨ b ≤ a

instance AddUnits.instLinearOrderedAddCommGroup {α : Type u_1} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommGroup (AddUnits α)

The units of a linearly ordered commutative additive monoid form a linearly ordered commutative additive group.

Equations

• AddUnits.instLinearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

theorem AddUnits.instLinearOrderedAddCommGroup.proof_3 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : min a b = if a ≤ b then a else b

theorem AddUnits.instLinearOrderedAddCommGroup.proof_5 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : compare a b = compareOfLessAndEq a b

theorem AddUnits.instLinearOrderedAddCommGroup.proof_4 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : max a b = if a ≤ b then b else a

theorem AddUnits.instLinearOrderedAddCommGroup.proof_1 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : AddUnits α) (b : AddUnits α) : a ≤ b → ∀ (c : AddUnits α), c + a ≤ c + b