subring vs submodule

Stream: maths

[Patrick Massot]

Let me bring up old news since it looks like the module refactor is almost done. The following works nicely:

import ring_theory.subring

variables {R : Type} [comm_ring R] (S : set R) [is_subring S]

example : comm_ring S := by apply_instance
example : has_add S := by apply_instance

Now add import linear_algebra.quotient_module at top, and the second example no-longer works. In particular this breaks the cast from nat to S. Is this fixed in the module refactor?

[Patrick Massot]

Let me bring up that thread. Kenny or Mario, do you think this problem is now fixed by the module refactor?

[Kenny Lau]

linear_algebra.quotient_module is deleted (and its content is migrated to linear_algebra.basic), so I imported that instead, and it worked