Module.End R M is a central algebra #
This file shows that the algebra of endomorphisms on a free module is central.
instance
Algebra.IsCentral.instEnd
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
:
IsCentral R (Module.End R M)
The center of endomorphisms on a free module is trivial, in other words, it is a central algebra.