Commit 2021-02-10 17:49 3fae96c9

View on Github →

feat(algebra/ordered_monoid): min_*_distrib (#6144) Also provide a canonically_linear_ordered_add_monoid instances for nat, nnreal, cardinal and with_top.

Estimated changes

Modified src/algebra/ordered_monoid.lean

added theorem min_mul_distrib'

added theorem min_mul_distrib

Modified src/data/nat/basic.lean

Modified src/data/real/nnreal.lean

Modified src/set_theory/cardinal.lean