Def Order.PartialIso.invOfIdeal

Modification history

2023-02-03 10:21

Mathlib/Order/CountableDenseLinearOrder.lean

feat port : Order.CountableDenseLinearOrder (#2037)

Added Order.PartialIso.invOfIdeal View on Github →