LeanPool.Monlib4.LinearAlgebra.Matrix.PiMat

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.Matrix.PiMat.

@[reducible, inline]

abbrev Mat (R : Type u_1) (n : Type u_2) : Type (max u_2 u_1)

Square matrices over R indexed by n.

Equations

• Mat R n = Matrix n n R

@[reducible, inline]

abbrev PiMat (R : Type u_1) (k : Type u_2) (s : k → Type u_3) : Type (max (max u_2 u_3) u_1)

Families of square matrices whose index type can vary with the family index.

Equations

• PiMat R k s = ((i : k) → (fun (j : k) => Mat R (s j)) i)

theorem PiMat.ext {R : Type u_1} {k : Type u_2} {s : k → Type u_3} {x y : PiMat R k s} (h : ∀ (i : k), x i = y i) : x = y

theorem PiMat.ext_iff {R : Type u_1} {k : Type u_2} {s : k → Type u_3} {x y : PiMat R k s} : x = y ↔ ∀ (i : k), x i = y i