single_mul_single — Mathlib

English

The product of two basis elements is again a basis element: (single a1 b1) * (single a2 b2) = single (a1 a2) (b1 a1 • b2).

Русский

Произведение двух базисных элементов снова даёт базисный элемент: (single a1 b1) * (single a2 b2) = single (a1 a2) (b1 a1 • b2).

LaTeX

$$$ (\mathrm{single}\; a_1\; b_1) * (\mathrm{single}\; a_2\; b_2) = \mathrm{single}\; (a_1 a_2)\; (b_1 \; a_1 \!\cdot b_2) $$$

Lean4

@[simp]
theorem single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} : (single a₁ b₁) * (single a₂ b₂) = single (a₁ * a₂) (b₁ * a₁ • b₂) :=
  (sum_single_index (by simp [zero_mul, single_zero, sum_zero])).trans
    (sum_single_index (by simp [smul_zero, mul_zero, single_zero]))

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