Theorems · Theorem · commutative algebra

contraction_of_isPowMul_of_boundedWrt

∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ]
  {β : Type u_3} [inst_3 : Ring β] (nα : F) {nβ : β → ℝ},
  IsPowMul nβ → ∀ {f : α →+* β}, RingHom.IsBoundedWrt (⇑nα) nβ f → ∀ (x : α), nβ (f x) ≤ nα x

If f : α →+* β is bounded with respect to a ring seminorm nα on α and a power-multiplicative function nβ : β → ℝ, then ∀ x : α, nβ (f x) ≤ nα x.

Defined in

Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingFunLikeRingSeminormClassRing