Theorem Ideal.comap_finsetInf

Modification history

2026-01-26 14:59
Mathlib/RingTheory/Ideal/Maps.lean
feat(RingTheory/Ideal/Maps): add `comap_finsetInf` (#34139) …
Added Ideal.comap_finsetInfView on Github →