mathlib
c8a2fd7f - feat(analysis/normed_space): normed_group punit (#7616)

Commit

4 years ago

feat(analysis/normed_space): normed_group punit (#7616) Minor content from LTE. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents