stabilizer — Mathlib

English

For an element a, the stabilizer is the subgroup of G that fixes a: { g ∈ G | g•a = a }.

Русский

Стабилизатор элемента a по действию G — это подгруппа всех g, таких что g•a = a.

LaTeX

$$def stabilizer (a : α) : Subgroup G := { stabilizerSubmonoid G a with inv_mem' := ... }$$

Lean4

/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
A subgroup. -/
@[to_additive /-- The stabilizer of an element under an action, i.e. what sends the element to
    itself. An additive subgroup. -/
    ]
def stabilizer (a : α) : Subgroup G :=
  { stabilizerSubmonoid G a with inv_mem' := fun {m} (ha : m • a = a) => show m⁻¹ • a = a by rw [inv_smul_eq_iff, ha] }

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