mem_intermediateField_iff — Mathlib

English

An element x lies in FixedPoints.intermediateField M if and only if every element of M fixes x.

Русский

Элемент x принадлежит FixedPoints.intermediateField M тогда и только тогда, когда каждый элемент M фиксирует x.

LaTeX

$$$x \in FixedPoints.intermediateField M \iff \forall m \in M, m\cdot x = x$$$

Lean4

@[simp]
theorem mem_intermediateField_iff {M : Type*} [Monoid M] [MulSemiringAction M E] [SMulCommClass M F E] {x : E} :
    x ∈ FixedPoints.intermediateField (F := F) M ↔ ∀ m : M, m • x = x :=
  .rfl

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