fixedBy — Mathlib

English

For each m ∈ M, fixedBy(m) is the set { x ∈ α | m • x = x } of elements fixed by m.

Русский

Для каждого элемента m ∈ M множество fixedBy(m) состоит из элементов x ∈ α such that m • x = x.

LaTeX

$$$$\\mathrm{fixedBy}(m) = \\{ x \\in \\alpha \\mid m \\cdot x = x \\}. $$$$

Lean4

/-- `fixedBy m` is the set of elements fixed by `m`. -/
@[to_additive /-- `fixedBy m` is the set of elements fixed by `m`. -/
    ]
def fixedBy (m : M) : Set α :=
  {x | m • x = x}

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