Theorems · Theorem · commutative algebra

eq_seminorms

∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ] {f g : F},
  IsPowMul ⇑f →
    IsPowMul ⇑g →
      (∃ r, ∃ (_ : 0 < r), ∀ (a : α), f a ≤ r * g a) → (∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a) → f = g

Given two power-multiplicative ring seminorms f, g on α, if f is bounded by a positive multiple of g and vice versa, then f = g.

Defined in

Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingFunLikeRingSeminormClass