Def HomogeneousIdeal.toIdeal

Modification history

2025-02-10 17:54
Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
feat(RingTheory/GradedAlgebra): define homogeneous submodule (#18728) …
Deleted HomogeneousIdeal.toIdealView on Github →
2023-05-21 14:57
Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean
feat: port RingTheory.GradedAlgebra.HomogeneousIdeal (#4159)
Added HomogeneousIdeal.toIdealView on Github →