Zulip Chat Archive

Stream: Is there code for X?

Topic: submodule.quotient.mk as a linear map?


view this post on Zulip Scott Morrison (Mar 29 2021 at 01:56):

Where is the bundled linear map corresponding to submodule.quotient.mk?

view this post on Zulip Scott Morrison (Mar 29 2021 at 01:58):

src#submodule.mkq

view this post on Zulip Scott Morrison (Mar 29 2021 at 01:59):

Gah, why is everything named completely differently when you switch from add_comm_group to module? :-(

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 02:00):

Feel free to rename ;)

view this post on Zulip Scott Morrison (Mar 29 2021 at 02:00):

Yeah... :-) I guess the add_comm_group stuff is old and junky and just be replaced with an API like for module?

view this post on Zulip Scott Morrison (Mar 29 2021 at 02:04):

There's also lots of basic stuff, like we have add_monoid_hom.of, but no linear_map.of.

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 02:30):

We have a non-typeclass docs#is_linear_map and a typeclass docs#is_monoid_hom

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 02:30):

I'm not sure which API is older.

view this post on Zulip Scott Morrison (Mar 29 2021 at 02:30):

is_monoid_hom is much older, predating monoid_hom.

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 02:31):

(I mean, add_comm_group is older but I'm not sure about various parts of submodule/is_submonoid API)

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 02:31):

Bundled monoid_homs and submonoids are definitely younger than typeclasses.

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 02:32):

And bundled submonoids are younger than submodules.


Last updated: May 07 2021 at 21:10 UTC