@[reducible, inline]

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

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)

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