Commit 2025-02-08 23:25 ecbdf17e

View on Github →

feat(Algebra/Order/Monoid/Canonical/Defs): dot notation aliases (#21197)

Estimated changes

added theorem one_lt_of_ne_one