le_iff_le — Mathlib

English

For intermediate field K and subgroup H, K ≤ fixedField H if and only if H ≤ fixingSubgroup K.

Русский

Для промежуточного поля K и подгруппы H: K ≤ fixedField(H) тогда и только тогда, когда H ≤ fixingSubgroup(K).

LaTeX

$$K \le fixedField H \iff H \le fixingSubgroup K$$

Lean4

theorem le_iff_le : K ≤ fixedField H ↔ H ≤ fixingSubgroup K :=
  ⟨fun h g hg x => h (Subtype.mem x) ⟨g, hg⟩, fun h x hx g => h (Subtype.mem g) ⟨x, hx⟩⟩

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