Theorem StrictMono.apply_eq

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