Theorem Mathlib.Tactic.Order.ToInt.exists_translation

Modification history

2025-11-16 16:31
Mathlib/Tactic/Order/ToInt.lean
feat(Tactic/Order): translate linear orders to `Int` (#26580) …
Added Mathlib.Tactic.Order.ToInt.exists_translationView on Github →