smul_def

Mathlib.GroupTheory.RegularWreathProduct

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

English

The explicit action formula is w · (λ, q) = ((w.left (w.right · q)) · λ, w.right · q).

Русский

Ясное формула действия: w · (λ, q) = ((w.left (w.right · q)) · λ, w.right · q).

LaTeX

$$$ w \cdot (\lambda, q) = \left( (w.left (w.right \cdot q)) \cdot \lambda, w.right \cdot q \right) $$$

Lean4

@[simp]
theorem smul_def {w : D ≀ᵣ Q} {p : Λ × Q} : w • p = ⟨(w.1 (w.2 * p.2)) • p.1, w.2 * p.2⟩ :=
  rfl

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

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

Разделы

Аффилиация

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