mathlib3
fb1787b1 - feat(analysis/seminorm): Group seminorms (#15594)

Commit

3 years ago

feat(analysis/seminorm): Group seminorms (#15594) Multiplicativize the existing `add_group_seminorm` material.

Author

YaelDillies

Parents