invariantExtension_apply — Mathlib

English

The invariantExtension applied to x equals the supremum of algNormOfAlgEquiv σ applied to x over all σ.

Русский

Применение invariantExtension к x равно супремуму algNormOfAlgEquiv σ на x по всем σ.

LaTeX

$$invariantExtension(K,L)(x) = \sup_{σ: L ≃ₐ[K] L} algNormOfAlgEquiv(σ)(x)$$

Lean4

@[simp]
theorem invariantExtension_apply (x : L) : invariantExtension K L x = iSup fun σ : L ≃ₐ[K] L ↦ algNormOfAlgEquiv σ x :=
  rfl

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