instMulActionProd

Mathlib.GroupTheory.RegularWreathProduct

URI: https://scilib.ai/kg/mathlib#RegularWreathProduct.instMulActionProd

English

The defined action yields a genuine MulAction: 1 · p = p and (w1 w2) · p = w1 · (w2 · p).

Русский

Задано корректное действие: 1 · p = p и (w1 w2) · p = w1 · (w2 · p).

LaTeX

$$$1 \cdot p = p \quad\text{and}\quad (w_1 w_2) \cdot p = w_1 \cdot (w_2 \cdot p).$$$

Lean4

instance : MulAction (D ≀ᵣ Q) (Λ × Q) where
  one_smul := by simp
  mul_smul := by simp [smul_smul, mul_assoc]

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

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

Разделы

Аффилиация

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