Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 07:05 1f5950a7

View on Github →

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

Estimated changes