Constructive simplicity of endomorphism algebras #
Every nonzero endomorphism of a finite-dimensional complex vector space
generates the full endomorphism algebra in the sense that it can be
"sandwiched" to produce the identity: there exist endomorphisms
U i, W i such that ∑ i, U i * A * W i = 1.
theorem
RS.exists_sum_conj_eq_one
{V : Type u_1}
[AddCommGroup V]
[Module ℂ V]
[FiniteDimensional ℂ V]
(A : Module.End ℂ V)
(hA : A ≠ 0)
:
The sandwich identity: a nonzero endomorphism generates the identity as a finite sum of two-sided products.