Theorems · Theorem · commutative algebra

eq_of_powMul_faithful

∀ {R : Type u_1} {S : Type u_2} [inst : NormedCommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f₁ : AlgebraNorm R S),
  IsPowMul ⇑f₁ →
    ∀ (f₂ : AlgebraNorm R S),
      IsPowMul ⇑f₂ →
        (∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x) →
          f₁ = f₂

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₂ [BGR, Proposition 3.1.5/1][bosch-guntzer-remmert].

Defined in

Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Cited by

1 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedCommRingCommRingAlgebra