mathlib3

028afe5d - chore(category/endomorphism): remove unneeded ext attribute (#16603)

chore(category/endomorphism): remove unneeded ext attribute (#16603) Removes an unnecessary `@[ext]` attribute that used an extended syntax which we are not planning to port to mathlib4. Closes #16602. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>