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]
def
with_top.linear_ordered_add_comm_group_with_top
{α : Type u_1}
[linear_ordered_add_comm_group α] :
Equations
- with_top.linear_ordered_add_comm_group_with_top = {le := linear_ordered_add_comm_monoid_with_top.le with_top.linear_ordered_add_comm_monoid_with_top, lt := linear_ordered_add_comm_monoid_with_top.lt with_top.linear_ordered_add_comm_monoid_with_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_add_comm_monoid_with_top.decidable_le with_top.linear_ordered_add_comm_monoid_with_top, decidable_eq := linear_ordered_add_comm_monoid_with_top.decidable_eq with_top.linear_ordered_add_comm_monoid_with_top, decidable_lt := linear_ordered_add_comm_monoid_with_top.decidable_lt with_top.linear_ordered_add_comm_monoid_with_top, max := linear_ordered_add_comm_monoid_with_top.max with_top.linear_ordered_add_comm_monoid_with_top, max_def := _, min := linear_ordered_add_comm_monoid_with_top.min with_top.linear_ordered_add_comm_monoid_with_top, min_def := _, add := linear_ordered_add_comm_monoid_with_top.add with_top.linear_ordered_add_comm_monoid_with_top, add_assoc := _, zero := linear_ordered_add_comm_monoid_with_top.zero with_top.linear_ordered_add_comm_monoid_with_top, zero_add := _, add_zero := _, nsmul := linear_ordered_add_comm_monoid_with_top.nsmul with_top.linear_ordered_add_comm_monoid_with_top, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, top := linear_ordered_add_comm_monoid_with_top.top with_top.linear_ordered_add_comm_monoid_with_top, le_top := _, top_add' := _, neg := option.map (λ (a : α), -a), sub := sub_neg_monoid.sub._default linear_ordered_add_comm_monoid_with_top.add with_top.linear_ordered_add_comm_group_with_top._proof_17 linear_ordered_add_comm_monoid_with_top.zero with_top.linear_ordered_add_comm_group_with_top._proof_18 with_top.linear_ordered_add_comm_group_with_top._proof_19 linear_ordered_add_comm_monoid_with_top.nsmul with_top.linear_ordered_add_comm_group_with_top._proof_20 with_top.linear_ordered_add_comm_group_with_top._proof_21 (option.map (λ (a : α), -a)), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default linear_ordered_add_comm_monoid_with_top.add with_top.linear_ordered_add_comm_group_with_top._proof_23 linear_ordered_add_comm_monoid_with_top.zero with_top.linear_ordered_add_comm_group_with_top._proof_24 with_top.linear_ordered_add_comm_group_with_top._proof_25 linear_ordered_add_comm_monoid_with_top.nsmul with_top.linear_ordered_add_comm_group_with_top._proof_26 with_top.linear_ordered_add_comm_group_with_top._proof_27 (option.map (λ (a : α), -a)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, exists_pair_ne := _, neg_top := _, add_neg_cancel := _}
@[simp, norm_cast]