Commit 2023-05-21 14:57 54991d4b

View on Github →

feat: port RingTheory.GradedAlgebra.HomogeneousIdeal (#4159)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean

added theorem HomogeneousIdeal.coe_bot

added theorem HomogeneousIdeal.coe_inf

added theorem HomogeneousIdeal.coe_sup

added theorem HomogeneousIdeal.coe_top

added theorem HomogeneousIdeal.eq_bot_iff

added theorem HomogeneousIdeal.eq_top_iff

added theorem HomogeneousIdeal.ext

added theorem HomogeneousIdeal.homogeneousHull_toIdeal_eq_self

added def HomogeneousIdeal.irrelevant

added theorem HomogeneousIdeal.isHomogeneous

added theorem HomogeneousIdeal.mem_iff

added theorem HomogeneousIdeal.mem_irrelevant_iff

added def HomogeneousIdeal.toIdeal

added theorem HomogeneousIdeal.toIdeal_add

added theorem HomogeneousIdeal.toIdeal_bot

added theorem HomogeneousIdeal.toIdeal_homogeneousCore_eq_self

added theorem HomogeneousIdeal.toIdeal_iInf

added theorem HomogeneousIdeal.toIdeal_iInf₂

added theorem HomogeneousIdeal.toIdeal_iSup

added theorem HomogeneousIdeal.toIdeal_iSup₂

added theorem HomogeneousIdeal.toIdeal_inf

added theorem HomogeneousIdeal.toIdeal_injective

added theorem HomogeneousIdeal.toIdeal_irrelevant

added theorem HomogeneousIdeal.toIdeal_mul

added theorem HomogeneousIdeal.toIdeal_sInf

added theorem HomogeneousIdeal.toIdeal_sSup

added theorem HomogeneousIdeal.toIdeal_sup

added theorem HomogeneousIdeal.toIdeal_top

added structure HomogeneousIdeal

added theorem Ideal.IsHomogeneous.bot

added theorem Ideal.IsHomogeneous.iInf₂

added theorem Ideal.IsHomogeneous.iSup₂

added theorem Ideal.IsHomogeneous.iff_eq

added theorem Ideal.IsHomogeneous.iff_exists

added theorem Ideal.IsHomogeneous.inf

added theorem Ideal.IsHomogeneous.mul

added theorem Ideal.IsHomogeneous.sInf

added theorem Ideal.IsHomogeneous.sSup

added theorem Ideal.IsHomogeneous.sup

added theorem Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self

added theorem Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self

added theorem Ideal.IsHomogeneous.top

added def Ideal.IsHomogeneous

added def Ideal.homogeneousCore'

added theorem Ideal.homogeneousCore'_eq_sSup

added theorem Ideal.homogeneousCore'_le

added theorem Ideal.homogeneousCore'_mono

added theorem Ideal.homogeneousCore.gc

added def Ideal.homogeneousCore.gi

added def Ideal.homogeneousCore

added theorem Ideal.homogeneousCore_eq_sSup

added theorem Ideal.homogeneousCore_mono

added theorem Ideal.homogeneousHull.gc

added def Ideal.homogeneousHull.gi

added def Ideal.homogeneousHull

added theorem Ideal.homogeneousHull_eq_iSup

added theorem Ideal.homogeneousHull_eq_sInf

added theorem Ideal.homogeneousHull_mono

added theorem Ideal.homogeneous_span

added theorem Ideal.isHomogeneous_iff_forall_subset

added theorem Ideal.isHomogeneous_iff_subset_iInter

added theorem Ideal.le_toIdeal_homogeneousHull

added theorem Ideal.mem_homogeneousCore_of_homogeneous_of_mem

added theorem Ideal.mul_homogeneous_element_mem_of_mem

added theorem Ideal.toIdeal_homogeneousCore_le

added theorem Ideal.toIdeal_homogeneousHull_eq_iSup