Module.End R M is a central algebra

This file shows that the algebra of endomorphisms on a free module is central.

theorem Module.End.mem_subsemiringCenter_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] {f : End R M} : f ∈ Subsemiring.center (End R M) ↔ ∃ (α : R) (hα : α ∈ Subsemiring.center R), f = smulLeft α hα

theorem Module.End.mem_subalgebraCenter_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [CommSemiring S] [Module S M] [SMulCommClass R S M] [Algebra S R] [IsScalarTower S R M] {f : End R M} : f ∈ Subalgebra.center S (End R M) ↔ ∃ (α : R) (hα : α ∈ Subalgebra.center S R), f = smulLeft α hα

instance Algebra.IsCentral.instEnd {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [CommSemiring S] [Module S M] [SMulCommClass R S M] [Algebra S R] [IsScalarTower S R M] [IsCentral S R] : IsCentral S (Module.End R M)

The center of endomorphisms on a free module is trivial, in other words, it is a central algebra.