Theorem HomogeneousIdeal.comap_mono

Modification history

2026-05-04 15:38
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Maps.lean
chore: tag (almost) all `mono` lemmas as `@[gcongr]` (#38793) …
Modified HomogeneousIdeal.comap_monoView on Github →
2026-03-05 10:25
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Maps.lean
feat(RingTheory): define maps of homogeneous ideals (#30334) …
Added HomogeneousIdeal.comap_monoView on Github →