base_smul_eq_smul

Mathlib.GroupTheory.PushoutI

URI: https://scilib.ai/kg/mathlib#Monoid.PushoutI.NormalWord.base_smul_eq_smul

English

The summand action is compatible with smul in the sense that hSMul distributes over word concatenation: (g1 g2) • w = g1 • (g2 • w).

Русский

Действие суммант совместимо с умножением по смулу: (g1 g2) • w = g1 • (g2 • w).

LaTeX

$$$$ \text{summand_smul_def} $$$$

Lean4

theorem base_smul_eq_smul (h : H) (w : NormalWord d) : base φ h • w = h • w := by rw [base_smul_def, base_smul_def']

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

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

Разделы

Аффилиация

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