Theorem not_lt_self

Modification history

2026-01-14 14:17
MathlibTest/ToDual.lean
feat(to_dual): linter for redundant uses of `to_dual`/`to_additive` (#33239) …
Deleted not_lt_selfView on Github →
2026-01-09 10:48
MathlibTest/ToDual.lean
fix(translate): don't unfold aux lemmas, but translate them (#33603) …
Modified not_lt_selfView on Github →
2025-11-25 01:06
MathlibTest/ToDual.lean
feat(translate): automatically infer the `(reorder := ...)` argument (#31902) …
Added not_lt_selfView on Github →