smul_coe

Mathlib.GroupTheory.GroupAction.Quotient

URI: https://scilib.ai/kg/mathlib#MulAction.Quotient.smul_coe

English

In the quotient, the class of b • q.out equals b • q.

Русский

В фактор-моде класс b • q.out равен b • q.

LaTeX

$$$\\operatorname{QuotientGroup.mk} (b \\cdot q_{out}) = b \\cdot q$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_coe [QuotientAction β H] (b : β) (a : α) : b • (a : α ⧸ H) = (↑(b • a) : α ⧸ H) :=
  rfl

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

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

Разделы

Аффилиация

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