Zulip Chat Archive

Stream: Is there code for X?

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

Scott Morrison (Mar 29 2021 at 01:56):

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

Scott Morrison (Mar 29 2021 at 01:58):

src#submodule.mkq

Scott Morrison (Mar 29 2021 at 01:59):

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

Yury G. Kudryashov (Mar 29 2021 at 02:00):

Feel free to rename ;)

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?

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.

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

Yury G. Kudryashov (Mar 29 2021 at 02:30):

I'm not sure which API is older.

Scott Morrison (Mar 29 2021 at 02:30):

is_monoid_hom is much older, predating monoid_hom.

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)

Yury G. Kudryashov (Mar 29 2021 at 02:31):

Bundled monoid_homs and submonoids are definitely younger than typeclasses.

Yury G. Kudryashov (Mar 29 2021 at 02:32):

And bundled submonoids are younger than submodules.

Last updated: Dec 20 2023 at 11:08 UTC