Theorem Submodule.comap_finsetInf

Modification history

2026-06-30 14:08
Mathlib/Algebra/Module/Submodule/Map.lean
feat(Algebra/Category/ModuleCat): submodules of presheaves of modules (#41159) …
Modified Submodule.comap_finsetInfView on Github →
2026-01-26 14:59
Mathlib/Algebra/Module/Submodule/Map.lean
feat(RingTheory/Ideal/Maps): add `comap_finsetInf` (#34139) …
Added Submodule.comap_finsetInfView on Github →