mathlib
7d287537 - chore(normed_space/weak_dual): generalize `normed_group` to `semi_normed_group` (#13914)

Commit

4 years ago

chore(normed_space/weak_dual): generalize `normed_group` to `semi_normed_group` (#13914) This almost halves the time this file takes to build, and is more general too.

Author

eric-wieser

Parents

86887539

mathlib 7d287537 - chore(normed_space/weak_dual): generalize `normed_group` to `semi_normed_group` (#13914)

mathlib
7d287537 - chore(normed_space/weak_dual): generalize `normed_group` to `semi_normed_group` (#13914)