fixingSubgroup_sup — Mathlib

English

The fixing subgroup of the join K ⊔ L is the intersection of fixing subgroups: (K ⊔ L).fixingSubgroup = K.fixingSubgroup ∩ L.fixingSubgroup.

Русский

Фиксирующая подгруппа объединения K ⊔ L совпадает с пересечением фиксационных подгрупп: (K ⊔ L).fixingSubgroup = K.fixingSubgroup ∩ L.fixingSubgroup.

LaTeX

$$$ (K \sqcup L).fixingSubgroup = K.fixingSubgroup \cap L.fixingSubgroup $$$

Lean4

theorem fixingSubgroup_sup {K L : IntermediateField F E} :
    (K ⊔ L).fixingSubgroup = K.fixingSubgroup ⊓ L.fixingSubgroup :=
  by
  ext φ
  exact
    ⟨fun h ↦ ⟨fixingSubgroup_antitone le_sup_left h, fixingSubgroup_antitone le_sup_right h⟩, by
      simp [← Subgroup.zpowers_le, ← IntermediateField.le_iff_le]⟩

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