Def Order.PartialIso.funOfIdeal

Modification history

2023-02-03 10:21

Mathlib/Order/CountableDenseLinearOrder.lean

feat port : Order.CountableDenseLinearOrder (#2037)

Added Order.PartialIso.funOfIdeal View on Github →