mathlib3
2a5a0b0e - feat(group_theory/*): mark some lemmas as ext (about homs out of free constructions) (#5484)

Commit

5 years ago

feat(group_theory/*): mark some lemmas as ext (about homs out of free constructions) (#5484) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

jcommelin

Parents