Mathlib Changelog
v4
Changelog
About
Github
Def
OrderIso.toInitialSeg
Modification history
2024-11-11 17:29
Mathlib/Order/InitialSeg.lean
chore(Order/InitialSeg): `InitialSeg.ofIso` → `RelIso.toInitialSeg` (#18069) …
Added
OrderIso.toInitialSeg
View on Github →