Theorems · Theorem · linear algebra

Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod

∀ {n : Type u_1} {p : Type u_2} {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (e : n ≃ p) (L : List (Matrix.TransvectionStruct n R)),
  (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.reindexEquiv e) L).prod =
    (Matrix.reindexAlgEquiv R R e) (List.map Matrix.TransvectionStruct.toMatrix L).prod

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableEqCommRingFintypeFintype