restrictRestrictAlgEquivMapHom_apply

English

If φ is an E-automorphism fixing L, and x lies in K, then the restriction map sends φ to φ restricted to x.

Русский

Если φ — автоморфизм E, фиксирующий L, и x ∈ K, то ограничение отображает φ на φ|_K(x).

LaTeX

$$$\bigl(\operatorname{restrictRestrictAlgEquivMapHom}(F,K,L,E)\;\varphi\bigr)(x) = \varphi(x)$ for all x ∈ K.$$

Lean4

@[simp]
theorem restrictRestrictAlgEquivMapHom_apply (φ : E ≃ₐ[L] E) (x : K) :
    restrictRestrictAlgEquivMapHom F K L E φ x = φ x := by
  simp [restrictRestrictAlgEquivMapHom, AlgEquiv.restrictNormalHom_apply]

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