isPowMul_invariantExtension — Mathlib

English

The invariantExtension norm is power-multiplicative.

Русский

Норма invariantExtension является степенной мультипликативной.

LaTeX

$$IsPowMul (invariantExtension K L)$$

Lean4

/-- The algebra norm `invariantExtension` is power-multiplicative. -/
theorem isPowMul_invariantExtension : IsPowMul (invariantExtension K L) :=
  by
  intro x n hn
  rw [invariantExtension_apply, invariantExtension_apply, Real.iSup_pow (fun σ ↦ apply_nonneg (algNormOfAlgEquiv σ) x)]
  exact iSup_congr fun σ ↦ isPowMul_algNormOfAlgEquiv σ _ hn

Похожие утверждения