mem_fixedField_iff — Mathlib

English

For fixedField H, x ∈ fixedField H iff every f ∈ H fixes x.

Русский

Для fixedField H верно: x ∈ fixedField H тогда и только тогда, когда каждый f ∈ H фиксирует x.

LaTeX

$$x ∈ fixedField H ↔ ∀ f ∈ H, f x = x$$

Lean4

@[simp]
theorem mem_fixedField_iff (x) : x ∈ fixedField H ↔ ∀ f ∈ H, f x = x :=
  by
  change x ∈ MulAction.fixedPoints H E ↔ _
  simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]

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