mathlib3
refactor(*): move `algebra` below `polynomial` in the `import` chain
#2294
Merged
Merged
refactor(*): move `algebra` below `polynomial` in the `import` chain #2294
mergify
merged
7 commits into
master
from
algebra-move
Move `algebra` below `polynomial` in the `import` chain
f2d9e13e
Fix compile
9b88dda3
Merge branch 'master' into algebra-move
9839f294
jcommelin
approved these changes
on 2020-03-31
bryangingechen
changed the title
bryangingechen
commented
on 2020-04-01
urkud
commented
on 2020-04-01
Update src/data/mv_polynomial.lean
7d26aad8
urkud
commented
on 2020-04-01
urkud
commented
on 2020-04-01
Apply suggestions from code review
614569ce
Apply suggestions from code review
6b8f2909
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into algebra-move
35c39aa7
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub