galRestrictHom_symm_algebraMap_apply

English

Applying galRestrictHom to σ and x gives the action of σ on x transported to B.

Русский

После применения galRestrictHom к σ и x действие σ на x переносится в B.

LaTeX

$$galRestrictHom_apply (σ : B →ₐ[A] B) (x : B) : algebraMap B L (galRestrictHom A K L B σ x) = σ (algebraMap B L x)$$

Lean4

@[simp, nolint unusedHavesSuffices] -- false positive from unfolding galRestrictHom

theorem galRestrictHom_symm_algebraMap_apply (σ : B →ₐ[A] B) (x : B) :
    (galRestrictHom A K L B).symm σ (algebraMap B L x) = algebraMap B L (σ x) :=
  galLift_algebraMap_apply _ _ _ _ _

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