coe_smul_out

Mathlib.GroupTheory.GroupAction.Quotient

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

English

The equality mk (smul_out) = smul_out holds, showing compatibility of mk and smul_out.

Русский

Равенство mk (smul_out) = smul_out демонстрирует совместимость mk и smul_out.

LaTeX

$$$\\text{mk\_smul\_out} = \\text{smul\_out}$$$

Lean4

@[to_additive]
theorem coe_smul_out [QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b • q.out) = b • q := by simp

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

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

Разделы

Аффилиация

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