Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 01:36 fbfdff7e

View on Github →

chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for inv (#11959) On Zulip it was decided that the name should be changed from ennreal.inv_order_iso to order_iso.inv_ennreal in order to better accord with the rest of the library.

Estimated changes