stabilizerSubmonoid — Mathlib

English

The stabilizer of a under M is the submonoid { m ∈ M | m • a = a }. It is closed under multiplication and contains 1.

Русский

Стабилизатор точки a под действием M — подморинод из элементов m ∈ M, удовлетворяющих m • a = a; замкнут относительно умножения и содержит единицу.

LaTeX

$$$$ \\operatorname{stabilizerSubmonoid}(M, a) = \\{ m \\in M \\mid m \\cdot a = a \\} $$$$

Lean4

/-- The stabilizer of a point `a` as a submonoid of `M`. -/
@[to_additive /-- The stabilizer of a point `a` as an additive submonoid of `M`. -/
    ]
def stabilizerSubmonoid (a : α) : Submonoid M
    where
  carrier := {m | m • a = a}
  one_mem' := one_smul _ a
  mul_mem' {m m'} (ha : m • a = a) (hb : m' • a = a) := show (m * m') • a = a by rw [← smul_smul, hb, ha]

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