mathlib3

d1e68751 - chore(algebra/category/Group/injective): remove redundant empty line (#16814)