Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 07:42 468c01c8

View on Github →

chore(topology/*): add two missing simp coe lemmas (#4748)

Estimated changes

Modified src/topology/algebra/module.lean

added theorem continuous_linear_equiv.coe_to_linear_equiv

Modified src/topology/metric_space/isometry.lean

added theorem isometric.coe_to_equiv