Commit 2024-07-18 08:58 8aa21118

feat(Analysis.Normed.Ring.SeminormFromBounded): add SeminormFromBounded (#14359) We prove [BGR, Proposition 1.2.1/2] : given a nonzero additive group seminorm on a commutative ring R such that for some positive c : ℝ and every x y : R, the inequality f (x * y) ≤ c * f x * f y) is satisfied, we create a ring seminorm on R.