mem_fixingSubgroup_iff — Mathlib

English

For any α ∈ Aut(K/k) and L ∈ FiniteGaloisIntermediateField(k,K), α lies in L.fixingSubgroup iff α.restrictNormalHom L = 1.

Русский

Для любой α ∈ Aut(K/k) и L ∈ FiniteGaloisIntermediateField(k,K), α ∈ L.fixingSubgroup тогда и только тогда, когда α|L = 1.

LaTeX

$$$ α ∈ L.fixingSubgroup \iff α.restrictNormalHom L = 1. $$$

Lean4

nonrec theorem mem_fixingSubgroup_iff (α : K ≃ₐ[k] K) (L : FiniteGaloisIntermediateField k K) :
    α ∈ L.fixingSubgroup ↔ α.restrictNormalHom L = 1 := by
  simp [IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
    AlgEquiv.restrictNormalHom_apply]

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