Structures · Algebra
AddSubmonoidClass
AddSubmonoidClass S M says S is a type of subsets s ≤ M that contain 0
and are closed under (+)
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by5
Concrete types that are instances5
- AddSubmonoid
- ClosedSubmodule
- SaturatedAddSubmonoid
- HomogeneousSubmodule
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by435
- HomogeneousIdeal
- HomogeneousIdeal.toIdeal
- DirectSum.decompose
- DirectSum.IsInternal
- sum_mem
- ProjectiveSpectrum.asHomogeneousIdeal
- ProjectiveSpectrum.basicOpen
- HomogeneousIdeal.irrelevant
- ProjectiveSpectrum.zeroLocus
- AddMonoidHom.domRestrict
- ProjectiveSpectrum.top
- HomogeneousIdeal.map
- Ideal.IsHomogeneous
- nsmul_mem
- GradedRing.proj
- ProjectiveSpectrum.vanishingIdeal
- HomogeneousSubmodule.toSubmodule
- DirectSum.decompose_coe
- AddSubmonoidClass.coe_finsetSum
- DirectSum.SetLike.IsHomogeneous
- DirectSum.decomposeAddEquiv
- ProjectiveSpectrum.gc_ideal
- DirectSum.decompose_mul
- AddSubmonoidClass.subtype
- Ideal.homogeneousCore
- list_sum_mem
- multiset_sum_mem
- HomogeneousIdeal.comap
- DirectSum.sum_support_decompose
- DirectSum.coeAddMonoidHom
- DirectSum.decomposeRingEquiv
- Submodule.IsHomogeneous
- Ideal.homogeneousHull
- DirectSum.decompose_of_mem
- DirectSum.decompose_symm_of
- DirectSum.decompose_of_mem_ne
- ProjectiveSpectrum.gc_set
- GradedRingHom.gradedAddHom
- HomogeneousSubsemiring.toSubsemiring
- GradedRing.projZeroRingHom
- DirectSum.Decomposition.isInternal
- DirectSum.decompose_of_mem_same
- HomogeneousIdeal.isHomogeneous
- AddSubmonoid.ofClass
- HomogeneousIdeal.toIdeal_injective
- ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
- AddMonoidHom.codRestrict
- DirectSum.degree_eq_of_mem_mem
- IsLinearTopology.mk_of_hasBasis'
- DirectSum.coe_mul_apply_eq_dfinsuppSum