Adjoining a top element to a linear_ordered_add_comm_group_with_top. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
The units of an ordered commutative additive monoid form an ordered commutative additive group.
Equations
- add_units.ordered_add_comm_group = {add := add_comm_group.add add_units.add_comm_group, add_assoc := _, zero := add_comm_group.zero add_units.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul add_units.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg add_units.add_comm_group, sub := add_comm_group.sub add_units.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul add_units.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le add_units.partial_order, lt := partial_order.lt add_units.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
The units of an ordered commutative monoid form an ordered commutative group.
Equations
- units.ordered_comm_group = {mul := comm_group.mul units.comm_group, mul_assoc := _, one := comm_group.one units.comm_group, one_mul := _, mul_one := _, npow := comm_group.npow units.comm_group, npow_zero' := _, npow_succ' := _, inv := comm_group.inv units.comm_group, div := comm_group.div units.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow units.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := partial_order.le units.partial_order, lt := partial_order.lt units.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}