transvection_mul_transvection_same

English

For i ≠ j, T_{ij}(c) T_{ij}(d) = T_{ij}(c + d).

Русский

Если i ≠ j, то транспекция умножается по c и d по правилу T_{ij}(c) T_{ij}(d) = T_{ij}(c + d).

LaTeX

$$$$ T_{ij}(c) T_{ij}(d) = T_{ij}(c + d) \\quad (i \\neq j). $$$$

Lean4

theorem transvection_mul_transvection_same (h : i ≠ j) (c d : R) :
    transvection i j c * transvection i j d = transvection i j (c + d) := by
  simp [transvection, Matrix.add_mul, Matrix.mul_add, h.symm, add_assoc, single_add]

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