mathlib3
6048b6f3 - feat(tactic/monotonicity): Allow `@[mono]` on `strict_mono` lemmas (#7017)

Commit

4 years ago

feat(tactic/monotonicity): Allow `@[mono]` on `strict_mono` lemmas (#7017) A follow-up to #3310

Author

eric-wieser

Parents