Theorems · Theorem · linear algebra

Matrix.mul_assoc

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalSemiring α]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α),
  L * M * N = L * (M * N)

Defined in: Mathlib.Data.Matrix.Mul
Cited by: 56 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NonUnitalSemiring Fintype Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
Matrix.extproof · cited by 540
NonUnitalSemiringstatement and proof · cited by 339
dotProduct_assocproof · cited by 3

Cited by56

Results whose statement or proof uses this declaration.

LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrictproof · cited by 8
LinearMap.det_conjproof · cited by 5
Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvecproof · cited by 3
LinearMap.traceAux_eqproof · cited by 3
Matrix.isHermitian_conjTranspose_mul_mulproof · cited by 3
Matrix.nonsing_inv_nonsing_invproof · cited by 3
Matrix.TransvectionStruct.reverse_inv_prod_mul_prodproof · cited by 3
Matrix.isRegular_of_isLeftRegular_detproof · cited by 3
Matrix.zpow_add_oneproof · cited by 3
Matrix.det_conj_of_mul_eq_oneproof · cited by 2
Matrix.conjTranspose_mul_self_mul_eq_zeroproof · cited by 2
SymplecticGroup.inv_left_mul_auxproof · cited by 2