galActionHom_restrict — Mathlib

English

If ϕ is an F-algebra automorphism of E, then the action via galActionHom composed with restrict p E coincides with applying ϕ to x.

Русский

Если ϕ — алгебраический автоморфизм E над F, то действие через galActionHom, затем через restrict p E, совпадает с действием ϕ на x.

LaTeX

$$$\\mathrm{galActionHom}(p,E)(\\mathrm{restrict}(p,E,\\varphi)\\, x) = \\varphi\\, x$$$

Lean4

theorem galActionHom_restrict [Fact (p.Splits (algebraMap F E))] (ϕ : E ≃ₐ[F] E) (x : rootSet p E) :
    ↑(galActionHom p E (restrict p E ϕ) x) = ϕ x :=
  restrict_smul ϕ x

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