Mathlib v3 is deprecated. Go to Mathlib v4

Def normed_add_comm_group.of_separation

Modification history

2022-10-06 17:50
src/analysis/normed/group/basic.lean
feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups (#15705) …
Deleted normed_add_comm_group.of_separationView on Github →
2022-08-16 10:36
src/analysis/normed/group/basic.lean
feat(analysis/normed/group/basic): construct a normed group from a seminormed group satisfying `∥x∥ = 0 → x = 0` (#16066) …
Added normed_add_comm_group.of_separationView on Github →