chore(src/algebra/lie/abelian): golf (#7898)
chore(src/algebra/lie/abelian): golf (#7898)

I golfed some of the proofs of the file `algebra/lie/abelian`.  My main motivation was to get familiar with the file.





leanprover-community/mathlib,leanprover-community/mathlib