fixingSubgroup — Mathlib

English

The fixingSubgroup of a subgroup H is the subgroup of automorphisms that fix the intermediate field K pointwise.

Русский

Фиксирующая подгруппа H — это подгруппа автоморфизмов, фиксирующая K поэлементно.

LaTeX

$$fixingSubgroup (E ≃ₐ[F] E) (K : IntermediateField F E)$$

Lean4

/-- The subgroup fixing an intermediate field. -/
nonrec def fixingSubgroup : Subgroup (E ≃ₐ[F] E) :=
  fixingSubgroup (E ≃ₐ[F] E) (K : Set E)

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