mathlib3
chore(algebra/group): streamlining imports
#2099
Merged

chore(algebra/group): streamlining imports #2099

mergify merged 4 commits into master from group_imports
kim-em
kim-em chore(algebra/group): streamlining imports
4de9cd16
kim-em reducing imports
95c975c0
cipher1024
kim-em
cipher1024
kim-em kim-em added awaiting-review
cipher1024 cipher1024 assigned ChrisHughes24 ChrisHughes24 6 years ago
cipher1024 cipher1024 unassigned ChrisHughes24 ChrisHughes24 6 years ago
cipher1024 cipher1024 assigned cipher1024 cipher1024 6 years ago
ChrisHughes24
ChrisHughes24 approved these changes on 2020-03-08
ChrisHughes24 ChrisHughes24 added ready-to-merge
ChrisHughes24 ChrisHughes24 removed awaiting-review
mergify[bot] Merge branch 'master' into group_imports
c94bb464
mergify[bot] Merge branch 'master' into group_imports
77c9c43c
mergify mergify merged 61d70ce8 into master 6 years ago
mergify mergify deleted the group_imports branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
Milestone