Zulip Chat Archive

Stream: new members

Topic: the third isomorphism theorem

Hbz (Aug 13 2025 at 08:19):

Does the third isomorphism theorem exist in mathllib, that is, something like (R/I)/(J/I) ≅ R/J?

Michael Rothgang (Aug 13 2025 at 08:24):

For groups, sure: docs#QuotientGroup.quotientQuotientEquivQuotient

Michael Rothgang (Aug 13 2025 at 08:25):

If it does exist for rings, a PR updating the library overview would be nice :-)

Michael Rothgang (Aug 13 2025 at 08:27):

Leansearch also finds e.g. docs#DoubleQuot.quotQuotEquivQuotOfLE

Michael Rothgang (Aug 13 2025 at 08:28):

And docs#DoubleQuot.quotQuotEquivQuotSup definition, which is what you want, I guess

Michael Rothgang (Aug 13 2025 at 08:29):

A PR documenting this better is welcome :-)

Hbz (Aug 13 2025 at 08:30):

I'll try my best. :joy:

Last updated: Dec 20 2025 at 21:32 UTC