Commit 2024-10-02 17:07 343c459e

feat(Analysis.Normed.Ring.IsPowMulFaithful): prove eq_of_powMul_faithful (#15445) We add AlgebraNorm and MulAlgebraNorm. We prove Bosch-Güntzer-Remmert, Proposition 3.1.5/1: if R is a normed commutative ring and f₁ and f₂ are two power-multiplicative R-algebra norms on S, then if f₁ and f₂ are equivalent on every subring R[y] for y : S, it follows that f₁ = f₂.