mathlib3
refactor(module/submodule): allow submodules to be used for sub-distrib_mul_actions
#6642
Open
Overview
Commits
14
Changes
View On GitHub

refactor(module/submodule): allow submodules to be used for sub-distrib_mul_actions #6642

eric-wieser wants to merge 14 commits into master from eric-wieser/relax-submodule
eric-wieser
eric-wieser refactor(module/submodule): allow submodules to be used for sub-distr…
ee7eedd2
eric-wieser eric-wieser requested a review from kbuzzard kbuzzard 4 years ago
eric-wieser tidy
f14ccfb7
eric-wieser fill in difficult underscore
0f0b4ebe
eric-wieser Fill in an "underscore"
38a38990
eric-wieser Eliminate a slow convert
e2721ab3
eric-wieser Add a missing lemma about alg_equiv conversions
a27742c1
eric-wieser guess
391ad51e
eric-wieser eric-wieser added blocked-by-other-PR
github-actions github-actions removed blocked-by-other-PR
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/relax-s…
4ab08eaf
eric-wieser fix
802ebe4c
eric-wieser fix
edba9bdb
bryangingechen bryangingechen added awaiting-review
github-actions github-actions added merge-conflict
bryangingechen bryangingechen removed awaiting-review
bryangingechen bryangingechen added awaiting-author
eric-wieser eric-wieser removed review request from kbuzzard kbuzzard 4 years ago
kbuzzard
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/relax-s…
51b3487b
github-actions github-actions removed merge-conflict
eric-wieser fix
259d66fd
eric-wieser Generalize to fix things
e2885706
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/relax-s…
076b6a6b
github-actions github-actions added merge-conflict
github-actions
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author merge-conflict too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum