fixingSubgroup_of_insert — Mathlib

English

There is a natural equivalence between fixingSubgroup after insertion and the mapped fixingSubgroup.

Русский

Существует естественный эквивалент между фиксирующей подгруппой после вставки и отображенной фиксирующей подгруппой.

LaTeX

$$$fixingSubgroup\ M\ (insert a (Subset.val'\ s)) \simeq\fixingSubgroup (stabilizer\ M\ a) s$$$

Lean4

@[to_additive]
theorem fixingSubgroup_of_insert (a : α) (s : Set (ofStabilizer M a)) :
    fixingSubgroup M (insert a ((fun x ↦ x.val) '' s)) =
      (fixingSubgroup (↥(stabilizer M a)) s).map (stabilizer M a).subtype :=
  by
  ext m
  simp [mem_fixingSubgroup_iff, mem_ofStabilizer_iff, subgroup_smul_def, and_comm]

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