Zulip Chat Archive

Stream: maths

Topic: Radical of an ideal

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

Sebastien Gouezel (Jan 16 2020 at 09:43):

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

Alex J. Best (Jan 16 2020 at 09:44):

Radicals are in ideal_operations.lean

Alex J. Best (Jan 16 2020 at 09:44):

I think the namespace is submodule

Alex J. Best (Jan 16 2020 at 09:45):

Only for comm_ring I think

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: Dec 20 2023 at 11:08 UTC