English
For any list L of transvections, the product of the reversed inverses times the original product equals 1: (L.reverse.map (toMatrix ∘ inv)).prod * (L.map toMatrix).prod = 1.
Русский
Для любого списка L трансвеκций произведение обратных элементов в обратном порядке умножения на исходное произведение равно 1.
LaTeX
$$$\\left(\\text{prod}_{t\\in L^{\\text{rev}}}\\, t^{-1}.\\text{toMatrix}\\right) \\cdot \\left(\\prod_{t\\in L}\\, t.\\text{toMatrix}\\right) = 1$$$
Lean4
theorem reverse_inv_prod_mul_prod (L : List (TransvectionStruct n R)) :
(L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (L.map toMatrix).prod = 1 := by
induction L with
| nil => simp
| cons t L
IH =>
suffices
(L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) * (L.map toMatrix).prod =
1
by simpa [Matrix.mul_assoc]
simpa [inv_mul] using IH
