toQuotient_apply

Mathlib.GroupTheory.GroupAction.Quotient

URI: https://scilib.ai/kg/mathlib#MulActionHom.toQuotient_apply

English

The canonical map to the quotient sends each group element g ∈ α to its coset g for the action.

Русский

Каноническая карта в фактор-множество отправляет каждый элемент группы g ∈ α в косет g.

LaTeX

$$$\\text{toQuotient}(H)(g) = g$$$

Lean4

@[simp]
theorem _root_.MulActionHom.toQuotient_apply (H : Subgroup α) (g : α) : MulActionHom.toQuotient H g = g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru