free_single_single — Mathlib

English

In the free module, the action on a double single delta corresponds to multiplication of the group elements: (free k G α) acts on single i (single h r) by single i (single (g h) r).

Русский

В свободном модуле действие на двойной базисный элемент δ соответствует умножению элементов группы: δ_g δ_h = δ_{gh} с сохранением коэффициента r.

LaTeX

$$$ free\, k\, G\, α\, g (single i (single h r)) = single i (single (g h) r) $$$

Lean4

theorem free_single_single (g h : G) (i : α) (r : k) :
    free k G α g (single i (single h r)) = single i (single (g * h) r) := by simp

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