Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-01 23:59 fdc3136d

View on Github →

feat(analysis/normed/group/basic): closure of {0} in a seminormed group (#17287)

Estimated changes

added theorem closure_one_eq