basic): remove `submodule_class` (#18902)

Commit

2 years ago

fix(algebra/module/submodule/basic): remove `submodule_class` (#18902) This is redundant in the face of `smul_mem_class`. This also adds a missing instance.

Author

eric-wieser

Parents

7317149f

mathlib3 8130e515 - fix(algebra/module/submodule/basic): remove `submodule_class` (#18902)

mathlib3
8130e515 - fix(algebra/module/submodule/basic): remove `submodule_class` (#18902)