Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-29 16:06 d032ed1d

View on Github →

feat(analysis/seminorm): Add construction of seminorm over normed fields (#15893) As for normed spaces the properties of seminorms over fields are strong enough so that it sufficies to assume that ∀ (r : 𝕜) x, f (r • x) ≤ ∥r∥ * f x. This PR adds this construction.

Estimated changes