mathlib

4063c236 - chore(algebra/algebra/basic): golf endomorphism_algebra