isNonarchimedean_algNormOfAlgEquiv

English

The invariantExtension norm is nonarchimedean.

Русский

Норма инвариантного расширения неархимедова.

LaTeX

$$IsNonarchimedean (invariantExtension K L)$$

Lean4

/-- The algebra norm `algNormOfAlgEquiv` is nonarchimedean. -/
theorem isNonarchimedean_algNormOfAlgEquiv (σ : L ≃ₐ[K] L) : IsNonarchimedean (algNormOfAlgEquiv σ) :=
  by
  intro x y
  simp only [algNormOfAlgEquiv_apply, map_add σ]
  exact
    (Classical.choose_spec
            (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hu.isNonarchimedean_norm)).2.2
      _ _

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