conjMap_ofFixingSubgroup_coe_apply

English

Conjugation map on fixingSubgroup evaluated at an element equals the action by g on that element.

Русский

Отображение конъюгации на фиксирующей подгруппе, примененное к элементу, равно действию g на этот элемент.

LaTeX

$$$conjMap_ofFixingSubgroup hg x = g\cdot (x)$$$

Lean4

@[to_additive (attr := simp)]
theorem conjMap_ofFixingSubgroup_coe_apply {hg : g • t = s} (x : ofFixingSubgroup M t) :
    conjMap_ofFixingSubgroup hg x = g • (x : α) :=
  rfl

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