Documentation

Mathlib.Algebra.Central.Matrix

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 ι] :
Equations
  • =