DefinitionsArchimedeanClass, addSubgroup, ballAddSubgroup, closedBallAddSubgroup, instInhabited, instLinearOrder, instOrderTop, liftOrderHom, lift₂, mk, orderHom, out, subsemigroup, ArchimedeanOrder, instInhabited, instLE, instLT, instPreorder, of, orderHom, val, FiniteArchimedeanClass, addSubgroup, ballAddSubgroup, closedBallAddSubgroup, congrOrderIso, liftOrderHom, mk, toUpperSetAddArchimedeanClass, withTopOrderIso, FiniteMulArchimedeanClass, ballSubgroup, closedBallSubgroup, congrOrderIso, liftOrderHom, mk, subgroup, toUpperSetMulArchimedeanClass, withTopOrderIso, MulArchimedeanClass, ballSubgroup, closedBallSubgroup, instInhabited, instLinearOrder, instOrderTop, liftOrderHom, lift₂, mk, orderHom, out, subgroup, subsemigroup, MulArchimedeanOrder, instInhabited, instLE, instLT, instPreorder, of, orderHom, val | 60 |
TheoremsaddSubgroup_antitone, addSubgroup_eq_bot, addSubgroup_strictAntiOn, archimedean_of_mk_eq_mk, ballAddSubgroup_antitone, ballAddSubgroup_top, closedBallAddSubgroup_top, forall, ind, instNontrivial, instSubsingleton, liftOrderHom_mk, lift_mk, lift₂_mk, lt_of_mk_lt_mk_of_nonneg, lt_of_mk_lt_mk_of_nonpos, map_mk_eq, map_mk_le, mem_addSubgroup_iff, mem_ballAddSubgroup_iff, mem_closedBallAddSubgroup_iff, min_le_mk_add, min_le_mk_of_le_of_le, min_le_mk_sub, mk_abs, mk_add_eq_mk_left, mk_add_eq_mk_right, mk_add_lt_mk_left_iff, mk_add_lt_mk_right_iff, mk_antitoneOn, mk_eq_mk, mk_eq_mk_of_archimedean, mk_eq_top_iff, mk_le_mk, mk_le_mk_iff_lt, mk_le_mk_of_abs, mk_left_le_mk_add, mk_left_le_mk_add_iff, mk_left_le_mk_sub, mk_left_le_mk_sub_iff, mk_lt_mk, mk_monotoneOn, mk_neg, mk_out, mk_right_le_mk_add, mk_right_le_mk_add_iff, mk_right_le_mk_sub, mk_right_le_mk_sub_iff, mk_sub_comm, mk_sub_eq_mk_left, mk_sub_eq_mk_right, mk_sub_lt_mk_left_iff, mk_sub_lt_mk_right_iff, mk_sum, mk_surjective, mk_zero, orderHom_injective, orderHom_mk, orderHom_top, out_top, pos_of_pos_of_mk_lt, range_mk, subsemigroup_eq_addSubgroup_of_ne_top, subsemigroup_strictAnti, top_eq_mk_iff, instNonempty, instSubsingleton, instTotalLe, le_def, lt_def, of_symm_eq, of_val, val_of, val_symm_eq, addSubgroup_eq_bot, addSubgroup_strictAnti, ballAddSubgroup_strictAnti, coe_congrOrderIso_apply, congrOrderIso_symm, ind, instNonemptyOfNontrivial, instSubsingletonOfAddArchimedean, liftOrderHom_mk, lift_mk, mem_addSubgroup_iff, mem_ballAddSubgroup_iff, mem_closedBallAddSubgroup_iff, min_le_mk_add, mk_le_mk, mk_lt_mk, mk_neg, subsemigroup_eq_addSubgroup, val_mk, withTopOrderIso_apply_coe, withTopOrderIso_symm_apply, ballSubgroup_strictAnti, coe_congrOrderIso_apply, congrOrderIso_symm, ind, instNonemptyOfNontrivial, instSubsingletonOfMulArchimedean, liftOrderHom_mk, lift_mk, mem_ballSubgroup_iff, mem_closedBallSubgroup_iff, mem_subgroup_iff, min_le_mk_mul, mk_inv, mk_le_mk, mk_lt_mk, subgroup_eq_bot, subgroup_strictAnti, subsemigroup_eq_subgroup, val_mk, withTopOrderIso_apply_coe, withTopOrderIso_symm_apply, ballSubgroup_antitone, ballSubgroup_top, closedBallSubgroup_top, forall, ind, instNontrivial, instSubsingleton, liftOrderHom_mk, lift_mk, lift₂_mk, lt_of_mk_lt_mk_of_le_one, lt_of_mk_lt_mk_of_one_le, map_mk_eq, map_mk_le, mem_ballSubgroup_iff, mem_closedBallSubgroup_iff, mem_subgroup_iff, min_le_mk_div, min_le_mk_mul, min_le_mk_of_le_of_le, mk_antitoneOn, mk_div_comm, mk_div_eq_mk_left, mk_div_eq_mk_right, mk_div_lt_mk_left_iff, mk_div_lt_mk_right_iff, mk_eq_mk, mk_eq_mk_of_mulArchimedean, mk_eq_top_iff, mk_inv, mk_le_mk, mk_le_mk_iff_lt, mk_le_mk_of_mabs, mk_left_le_mk_div, mk_left_le_mk_div_iff, mk_left_le_mk_mul, mk_left_le_mk_mul_iff, mk_lt_mk, mk_mabs, mk_monotoneOn, mk_mul_eq_mk_left, mk_mul_eq_mk_right, mk_mul_lt_mk_left_iff, mk_mul_lt_mk_right_iff, mk_one, mk_out, mk_prod, mk_right_le_mk_div, mk_right_le_mk_div_iff, mk_right_le_mk_mul, mk_right_le_mk_mul_iff, mk_surjective, mulArchimedean_of_mk_eq_mk, one_lt_of_one_lt_of_mk_lt, orderHom_injective, orderHom_mk, orderHom_top, out_top, range_mk, subgroup_antitone, subgroup_eq_bot, subgroup_strictAntiOn, subsemigroup_eq_subgroup_of_ne_top, subsemigroup_strictAnti, top_eq_mk_iff, instNonempty, instSubsingleton, instTotalLe, le_def, lt_def, of_symm_eq, of_val, val_of, val_symm_eq | 190 |