Theorem HomogeneousIdeal.gc_map_comap

Modification history

2026-03-05 10:25
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Maps.lean
feat(RingTheory): define maps of homogeneous ideals (#30334) …
Added HomogeneousIdeal.gc_map_comapView on Github →