isPowMul_algNormOfAlgEquiv — Mathlib

English

The invariantExtension norm is power-multiplicative.

Русский

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

LaTeX

$$IsPowMul (invariantExtension K L)$$

Lean4

/-- The algebra norm `algNormOfAlgEquiv` is power-multiplicative. -/
theorem isPowMul_algNormOfAlgEquiv (σ : L ≃ₐ[K] L) : IsPowMul (algNormOfAlgEquiv σ) :=
  by
  intro x n hn
  simp only [algNormOfAlgEquiv_apply, map_pow σ x n]
  exact
    (Classical.choose_spec
          (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hu.isNonarchimedean_norm)).1
      _ hn

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