prod_mul_reverse_inv_prod — Mathlib

English

Equivalently, the product of transvection matrices times the reverse product of their inverses equals 1: (L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ inv)).prod = 1.

Русский

Эквивалентно, произведение матриц трансвеκций умноженное на обратное произведение их обратных равно 1.

LaTeX

$$$(\\prod_{t\\in L} t.toMatrix) \\cdot (\\prod_{t\\in L^{\\text{rev}}} t.inv.toMatrix) = 1$$$

Lean4

theorem prod_mul_reverse_inv_prod (L : List (TransvectionStruct n R)) :
    (L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod = 1 := by
  induction L with
  | nil => simp
  | cons t L
    IH =>
    suffices
      t.toMatrix * ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) * t.inv.toMatrix =
        1
      by simpa [Matrix.mul_assoc]
    simp_rw [IH, Matrix.mul_one, t.mul_inv]

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