coe_galRestrict_apply — Mathlib

English

The symmetric part of galRestrictHom respects the algebra map when evaluated on x.

Русский

Симметрическая часть galRestrictHom сохраняет алгебраическую карту при применении к x.

LaTeX

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

Lean4

theorem coe_galRestrict_apply (σ : L ≃ₐ[K] L) : (galRestrict A K L B σ : B →ₐ[A] B) = galRestrictHom A K L B σ :=
  rfl

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