Theorem StrictMono.eq_id

Modification history

2026-07-13 17:10
Mathlib/Order/Preorder/Finite.lean
feat(Order/OrderIsoNat+Data/Finset/Sort): add finiteness and identity theorems for linear orders (#41679) …
Added StrictMono.eq_idView on Github →