LeanPool.Monlib4.LinearAlgebra.Matrix.Cast #

theorem Matrix.cast_apply {R : Type u_1} {k : Type u_2} {s : k → Type u_3} {i j : k} (x : Matrix (s i) (s i) R) (h : i = j) (p q : s j) :

⋯.mp x p q = x (⋯.mpr p) (⋯.mpr q)

theorem Matrix.cast_apply' {R : Type u_1} {k : Type u_2} {s : k → Type u_3} {i j : k} (x : Matrix (s j) (s j) R) (h : j = i) (p q : s i) :

⋯.mpr x p q = x (⋯.mpr p) (⋯.mpr q)

theorem Matrix.cast_hMul {R : Type u_1} {k : Type u_2} {s : k → Type u_3} [Semiring R] [(i : k) → Fintype (s i)] {i j : k} (x y : Matrix (s i) (s i) R) (h : i = j) :

⋯.mp (x * y) = ⋯.mp x * ⋯.mp y