Commit 2025-05-23 00:25 1a437a5a
View on Github →feat: more results about Ideal.prod
(#25118)
From [#Is there code for X? > `Ideal.prod_span` version for different rings @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60Ideal.2Eprod_span.60.20version.20for.20different.20rings/near/519839282)