mathlib3
ecb5c5f5 - docs(algebra/module): Remove completed TODO (#3690)

Commit

5 years ago

docs(algebra/module): Remove completed TODO (#3690) Today, submodule _does_ extend `add_submonoid`, which is I assume what this TODO was about

Author

eric-wieser

Parents