Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-21 17:46 7944cc55

View on Github →

fix(*): fix some problems introduced with 98152392bcd4b3f783602d030a5ab6a9e47e0088 and 9aec1d18d3c4cbad400d7ddcdd63b94d647b0a01

Estimated changes

Modified analysis/metric_space.lean

Modified analysis/normed_space.lean

Modified analysis/topology/topological_space.lean

Modified linear_algebra/submodule.lean

Modified order/order_iso.lean

modified theorem order_iso.coe_coe_fn

Modified set_theory/cofinality.lean

Modified set_theory/ordinal.lean

modified theorem initial_seg.coe_coe_fn

modified theorem principal_seg.coe_coe_fn'

modified theorem principal_seg.coe_coe_fn