mathlib
f2259302 - chore(group_theory/*): Golf using `subgroup.subtype_injective` (#16941)

Commit

3 years ago

chore(group_theory/*): Golf using `subgroup.subtype_injective` (#16941) This PR uses the recently added `subgroup.subtype_injective` to golf a few lines.

Author

tb65536

Parents

8f82d25e

mathlib f2259302 - chore(group_theory/*): Golf using `subgroup.subtype_injective` (#16941)

mathlib
f2259302 - chore(group_theory/*): Golf using `subgroup.subtype_injective` (#16941)