Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 12:26 1f992c92

View on Github →

fix(.): adapt to Lean changes: type class parameters to structures are now type class parameters in the projections and constructor

Estimated changes

Modified algebra/module.lean

modified theorem mul_smul

modified theorem smul_left_distrib

modified theorem smul_right_distrib

Modified data/fp/basic.lean

modified def fp.float.default_nan

Modified order/basic.lean

Modified topology/topological_space.lean

modified theorem t2_separation

Modified topology/topological_structures.lean