mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open eric-wieser opened this issue 4 years ago • 2 comments

  • [x] depends on: #6648

note that this only deals with submonoids closed under smul, not subgroups closed under smul; I know one of @kbuzzard's students is working on the latter.

This is getting stuck on some timeouts in hahn_banach

eric-wieser avatar Mar 11 '21 16:03 eric-wieser

My student wrote some wholly non-mathlib-ready code and I think they're done.

kbuzzard avatar Mar 22 '21 19:03 kbuzzard

This PR/issue depends on:

  • ~~leanprover-community/mathlib#6648~~ By Dependent Issues (🤖). Happy coding!

github-actions[bot] avatar Dec 25 '21 12:12 github-actions[bot]