Theorems · Theorem · linear algebra

Matrix.reindexLinearEquiv_comp_apply

∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n')
  (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') (M : Matrix m n A),
  (Matrix.reindexLinearEquiv R A e₁' e₂') ((Matrix.reindexLinearEquiv R A e₁ e₂) M) =
    (Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) M

Defined in

Mathlib.LinearAlgebra.Matrix.Reindex

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModule