isNonarchimedean_invariantExtension

English

The invariantExtension is nonarchimedean.

Русский

Инвариантное расширение неархимедово.

LaTeX

$$IsNonarchimedean (invariantExtension K L)$$

Lean4

/-- The algebra norm `invariantExtension` is nonarchimedean. -/
theorem isNonarchimedean_invariantExtension : IsNonarchimedean (invariantExtension K L) := fun x y ↦
  ciSup_le fun σ ↦
    le_trans (isNonarchimedean_algNormOfAlgEquiv σ x y)
      (max_le_max (le_ciSup_of_le (Set.finite_range _).bddAbove σ (le_refl _))
        (le_ciSup_of_le (Set.finite_range _).bddAbove σ (le_refl _)))

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