mathlib3
4e9b18b6 - chore(order/basic): rename monotone_of_monotone_nat and strict_mono.nat (#8550)

Commit
4 years ago
chore(order/basic): rename monotone_of_monotone_nat and strict_mono.nat (#8550) For more coherence (and easier discoverability), rename `monotone_of_monotone_nat` to `monotone_nat_of_le_succ`, and `strict_mono.nat` to `strict_mono_nat_of_lt_succ`.
Author
Parents
Loading