mathlib3

2f93d81c - feat(logic/equiv/transfer_instances, group_theory/eckmann_hilton): make definitions reducible (#16884)

feat(logic/equiv/transfer_instances, group_theory/eckmann_hilton): make definitions reducible (#16884) Make `equiv.has_one` etc. reducible, which is necessary to use these defs to construct instances; the check_reducibility linter will complain about "semireducible non-instances" if these are not marked reducible. [function.injective.comm_group](https://leanprover-community.github.io/mathlib_docs/algebra/group/inj_surj.html#function.injective.comm_group) etc. are already made reducible and used to construct instances.