mem_fixingSubgroup_insert_iff — Mathlib

English

For a given a and a set s of fixingStabilizer elements, the fixingSubgroup for the inserted element equals the mapped fixingSubgroup.

Русский

Для данного a и множества s элементов FixingStabilizer фиксирующая подгруппа при вставке совпадает с отображаемойfixingSubgroup.

LaTeX

$$$fixingSubgroup\ M\ (insert\ a\ s) = (fixingSubgroup\ (Stabilizer\ M\ a)\ s).map\ (stabilizer\ M\ a).subtype$$$

Lean4

@[to_additive]
theorem mem_fixingSubgroup_insert_iff {a : α} {s : Set α} {m : M} :
    m ∈ fixingSubgroup M (insert a s) ↔ m • a = a ∧ m ∈ fixingSubgroup M s := by simp [mem_fixingSubgroup_iff]

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