Commit 2026-01-26 14:59 b8ccc79e
View on Github →feat(RingTheory/Ideal/Maps): add comap_finsetInf (#34139)
This PR adds an API lemma specializing comap_iInf to the case of finsets, which I've found helpful for working with primary decomposition.