orbitEquivQuotientStabilizer_symm_apply

English

The inverse of the orbit-stabilizer equivalence sends a group element to its action on the base element.

Русский

Обратное к эквивалентности орбиты и стабилизатора отправляет элемент группы к действию на базовый элемент.

LaTeX

$$$((\\operatorname{orbitEquivQuotientStabilizer}(\\alpha,b)).symm a : \\beta) = a \\cdot b$$$

Lean4

@[to_additive (attr := simp)]
theorem orbitEquivQuotientStabilizer_symm_apply (b : β) (a : α) :
    ((orbitEquivQuotientStabilizer α b).symm a : β) = a • b :=
  rfl

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