Commit 2024-09-05 20:53 3fbe1a09

View on Github →

feat: Add LinearOrderedCommMonoidWithZero and lemmas for unitInterval (#15436)

Estimated changes

Modified Mathlib/Topology/UnitInterval.lean

added theorem unitInterval.coe_lt_one

modified theorem unitInterval.coe_ne_one

modified theorem unitInterval.coe_ne_zero

added theorem unitInterval.coe_pos

added theorem unitInterval.eq_one_or_eq_zero_of_le_mul

added theorem unitInterval.le_symm_comm

added theorem unitInterval.lt_symm_comm

added theorem unitInterval.symm_eq_one

added theorem unitInterval.symm_eq_zero

added theorem unitInterval.symm_inj

added theorem unitInterval.symm_le_comm

added theorem unitInterval.symm_le_symm

added theorem unitInterval.symm_lt_comm

added theorem unitInterval.symm_lt_symm