Theorem unitInterval.eq_one_or_eq_zero_of_le_mul

Modification history

2024-09-05 20:53
Mathlib/Topology/UnitInterval.lean
feat: Add LinearOrderedCommMonoidWithZero and lemmas for unitInterval (#15436)
Added unitInterval.eq_one_or_eq_zero_of_le_mulView on Github →