map_id — Mathlib

English

The size of the finite Galois intermediate field has a finite correspondence with the finiteness of automorphisms.

Русский

Размер конечного Галуа-подполя имеет соответствие с конечностью автоморфизмов.

LaTeX

$$|finGaloisGroup(L)| = Finite$$

Lean4

@[simp]
theorem map_id (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) : (finGaloisGroupMap (𝟙 L)) = 𝟙 L.unop.finGaloisGroup :=
  ConcreteCategory.ext (AlgEquiv.restrictNormalHom_id _ _)

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