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)

Estimated changes

added theorem Ideal.coe_prod
modified theorem Ideal.mem_prod
deleted theorem Ideal.prod.ext_iff
added theorem Ideal.prod_bot_bot
added theorem Ideal.prod_eq_bot_iff
added theorem Ideal.prod_eq_top_iff
added theorem Ideal.prod_inj
added theorem Ideal.prod_mono
added theorem Ideal.prod_mono_left
added theorem Ideal.prod_mono_right
added theorem Ideal.span_prod
added theorem Ideal.span_prod_le