Theorem Mathlib.Tactic.Order.ToInt.toInt_le_toInt

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.toInt_le_toIntView on Github →