galLift_algebraMap_apply — Mathlib

English

The lift of galRestrict' is the original map: galLift(galRestrict'(σ)) = σ.

Русский

Подъем galRestrict' надлежащим образом восстанавливает исходное отображение: galLift(galRestrict'(σ)) = σ.

LaTeX

$$galLift_galRestrict'(σ) : galLift K L L₂ (galRestrict' A B B₂ σ) = σ$$

Lean4

@[simp]
theorem galLift_algebraMap_apply (σ : B →ₐ[A] B₂) (x : B) :
    galLift K L L₂ σ (algebraMap B L x) = algebraMap B₂ L₂ (σ x) := by simp [galLift]

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