mathlib3 documentation

algebra.order.group.units

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.