Zulip Chat Archive

Stream: maths

Topic: subring vs submodule


view this post on Zulip Patrick Massot (Oct 09 2018 at 12:16):

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?

view this post on Zulip Patrick Massot (Nov 03 2018 at 17:14):

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

view this post on Zulip Kenny Lau (Nov 03 2018 at 17:45):

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


Last updated: May 10 2021 at 07:15 UTC