The matrix algebra is a central algebra #
instance
Algebra.IsCentral.matrix
(K : Type u_1)
(D : Type u_2)
[CommSemiring K]
[Semiring D]
[Algebra K D]
[Algebra.IsCentral K D]
(ι : Type u_3)
[Fintype ι]
[DecidableEq ι]
:
Algebra.IsCentral K (Matrix ι ι D)
Equations
- ⋯ = ⋯