Structures · Algebra
SetLike.GradedSMul
A version of GradedMonoid.GSMul for internally graded objects.
- Defined in
- Mathlib.Algebra.GradedMulAction
- Shape
- 2 explicit arguments · adds smul_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- HomogeneousSubmodule.toSubmodule
- HomogeneousSubmodule.is_homogeneous'
- HomogeneousSubmodule.toSubmodule_injective
- HomogeneousSubmodule.ext'
- HomogeneousSubmodule.mk.congr_simp
- SetLike.GradedSMul.smul_mem
- HomogeneousSubmodule.isHomogeneous
- SetLike.IsHomogeneousElem.graded_smul
- HomogeneousSubmodule.setLike
- instPartialOrderHomogeneousSubmodule_1
- SetLike.gmulAction
- HomogeneousSubmodule.mem_toSubmodule_iff
- SetLike.toGSMul
- instSMulMemClassHomogeneousSubmodule
- SetLike.gmodule
- GradedModule.isModule
- instAddSubmonoidClassHomogeneousSubmodule
- GradedModule.linearEquiv
- SetLike.coe_GSMul
- SetLike.gdistribMulAction
- IsModuleFiltration.mk_int
- instPartialOrderHomogeneousSubmodule
- instSetLikeHomogeneousSubmodule
Ancestors0
No ancestors.