mathlib3
1f5950a7 - feat(analysis/seminorm): add lemmas for `with_seminorms` (#12649)

Commit

3 years ago

feat(analysis/seminorm): add lemmas for `with_seminorms` (#12649) Two helper lemmas that make it easier to generate an instance for `with_seminorms`.

Author

mcdoll

Parents