Zulip Chat Archive

Stream: maths

Topic: Radical of an ideal


view this post on Zulip Kevin Buzzard (Jan 16 2020 at 09:41):

Do we have radical of an ideal in mathlib? I tried ideal.radical and it wasn't there. Do I need an import? I am so bad at search

view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 09:43):

There is #768, waiting for someone to clean it up. Is that what you want?

view this post on Zulip Alex J. Best (Jan 16 2020 at 09:44):

Radicals are in ideal_operations.lean

view this post on Zulip Alex J. Best (Jan 16 2020 at 09:44):

I think the namespace is submodule

view this post on Zulip Alex J. Best (Jan 16 2020 at 09:45):

Only for comm_ring I think

view this post on Zulip Kevin Buzzard (Jan 16 2020 at 12:29):

Alex: Oh thanks! I'm a twit; I could have just searched mathlib for "radical". Sebastien -- I might need something about Jacobson rings soon so I might have to turn my attention to that PR.


Last updated: May 09 2021 at 10:11 UTC