fixingSubgroup — Mathlib

English

The subgroup fixing a set s is the collection of elements of M that fix every element of s under the action.

Русский

Подгруппа, фиксирующая множество s, состоит из элементов M, которые фиксируют каждый элемент s при действии.

LaTeX

$$$fixingSubgroup(M,s) = \\{ x \\in M \\mid \\forall y \\in s:\\; x \\cdot y = y \\}$$$

Lean4

/-- The subgroup fixing a set under a `MulAction`. -/
@[to_additive /-- The additive subgroup fixing a set under an `AddAction`. -/
    ]
def fixingSubgroup (s : Set α) : Subgroup M :=
  { fixingSubmonoid M s with inv_mem' := fun hx z => by rw [inv_smul_eq_iff, hx z] }

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