Mathlib v3 is deprecated. Go to Mathlib v4

Theorem enorm.coe_inj

Modification history

2021-10-21 02:55

src/analysis/normed_space/enorm.lean

chore(*): bump to lean 3.34.0 (#9824) …

Modified enorm.coe_inj View on Github →

2020-10-20 10:23

src/analysis/normed_space/enorm.lean

chore(*): review some lemmas about injectivity of coercions (#4711) …

Added enorm.coe_inj View on Github →