fixingSubgroup_top — Mathlib

English

The fixing subgroup of the largest intermediate field (the top) is the bottom subgroup (the trivial group).

Русский

Фиксирующая подгруппа на верхнем промежуточном поле равна нулевой подгруппе (тривиальная подгруппа).

LaTeX

$$$\operatorname{fixingSubgroup}(\top)=\bot$$$

Lean4

@[simp]
theorem fixingSubgroup_top : fixingSubgroup (⊤ : IntermediateField F E) = ⊥ :=
  by
  ext
  simp [DFunLike.ext_iff]

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