galRestrict_apply — Mathlib

English

If σ is an AlgEquiv, galRestrict maps σ to an AlgEquiv, preserving algebra maps.

Русский

Если σ — АлгЭкв, galRestrict отображает σ в АлгЭкв, сохраняющий алгебраические отображения.

LaTeX

$$galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) : galRestrict A K L B σ x = galRestrictHom A K L B σ x$$

Lean4

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

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