spectralNorm_eq_of_equiv — Mathlib

English

If σ is an algebra isomorphism of L over K, then spectralNorm(K,L)(x) = spectralNorm(K,L)(σ x).

Русский

Если σ является алгебраическим изоморфизмом L над K, то spectralNorm(K,L)(x) = spectralNorm(K,L)(σ x).

LaTeX

$$$$\operatorname{spectralNorm}(K,L)(x)=\operatorname{spectralNorm}(K,L)(σ x).$$$$

Lean4

/-- The `K`-algebra automorphisms of `L` are isometries with respect to the spectral norm. -/
theorem spectralNorm_eq_of_equiv (σ : L ≃ₐ[K] L) (x : L) : spectralNorm K L x = spectralNorm K L (σ x) := by
  simp only [spectralNorm, minpoly.algEquiv_eq]
    -- We first assume that the extension is finite and normal

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