fin_two_smul_prod — Mathlib

English

Let g be a 2×2 matrix over a ring R and v = (v1, v2) a pair in R×R. The action is the standard left-multiplication, i.e. g • v = (g11 v1 + g12 v2, g21 v1 + g22 v2).

Русский

Пусть g — матрица 2×2 над кольцом R, а v = (v1,v2) ∈ R×R. Действие задаётся обычным левым умножением: g • v = (g11 v1 + g12 v2, g21 v1 + g22 v2).

LaTeX

$$$g\\cdot (v_1,v_2) = (g_{00}v_1+g_{01}v_2,\\; g_{10}v_1+g_{11}v_2).$$$

Lean4

@[simp]
theorem fin_two_smul_prod (g : Matrix (Fin 2) (Fin 2) R) (v : R × R) :
    g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2) := by
  simp [Equiv.smul_def, smul_eq_mulVec, Matrix.mulVec_eq_sum]

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