GradedModule

📁 Source: Mathlib/Algebra/Module/GradedModule.lean

Statistics

Metric	Count
Definitions toGmodule, GdistribMulAction, toGMulAction, Gmodule, instSMulOfDecidableEq, smulAddMonoidHom, toGdistribMulAction, gsmulHom, isModule, linearEquiv, gdistribMulAction, gmodule, gmulAction	13
Theorems smul_add, smul_zero, add_smul, of_smul_of, smulAddMonoidHom_apply_of_of, smul_def, zero_smul, gsmulHom_apply_apply	8
Total	21

DirectSum

Definitions

Name	Category	Theorems
GdistribMulAction 📖	CompData	—
Gmodule 📖	CompData	—
gsmulHom 📖	CompOp	1 math math: gsmulHom_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gsmulHom_apply_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom HVAdd.hVAdd instHVAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike AddMonoidHom.instAddCommMonoid gsmulHom GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul GdistribMulAction.toGMulAction Gmodule.toGdistribMulAction	—	—

DirectSum.GSemiring

Definitions

Name	Category	Theorems
toGmodule 📖	CompOp	—

DirectSum.GdistribMulAction

Definitions

Name	Category	Theorems
toGMulAction 📖	CompOp	7 math math: DirectSum.Gmodule.smulAddMonoidHom_apply_of_of, DirectSum.Gmodule.of_smul_of, smul_zero, DirectSum.Gmodule.zero_smul, DirectSum.gsmulHom_apply_apply, smul_add, DirectSum.Gmodule.add_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_add 📖	mathematical	—	GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul toGMulAction AddSemigroup.toAdd AddMonoid.toAddSemigroup HVAdd.hVAdd instHVAdd	—	—
smul_zero 📖	mathematical	—	GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul toGMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass HVAdd.hVAdd instHVAdd	—	—

DirectSum.Gmodule

Definitions

Name	Category	Theorems
instSMulOfDecidableEq 📖	CompOp	2 math math: of_smul_of, smul_def
smulAddMonoidHom 📖	CompOp	2 math math: smulAddMonoidHom_apply_of_of, smul_def
toGdistribMulAction 📖	CompOp	5 math math: smulAddMonoidHom_apply_of_of, of_smul_of, zero_smul, DirectSum.gsmulHom_apply_apply, add_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_smul 📖	mathematical	—	GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul DirectSum.GdistribMulAction.toGMulAction toGdistribMulAction AddSemigroup.toAdd AddMonoid.toAddSemigroup HVAdd.hVAdd instHVAdd	—	—
of_smul_of 📖	mathematical	—	DirectSum instSMulOfDecidableEq DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of HVAdd.hVAdd instHVAdd GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul DirectSum.GdistribMulAction.toGMulAction toGdistribMulAction	—	smulAddMonoidHom_apply_of_of
smulAddMonoidHom_apply_of_of 📖	mathematical	—	DFunLike.coe AddMonoidHom DirectSum AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike AddMonoidHom.instAddCommMonoid smulAddMonoidHom DirectSum.of HVAdd.hVAdd instHVAdd GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul DirectSum.GdistribMulAction.toGMulAction toGdistribMulAction	—	DirectSum.toAddMonoid_of
smul_def 📖	mathematical	—	DirectSum instSMulOfDecidableEq DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike AddMonoidHom.instAddCommMonoid smulAddMonoidHom	—	—
zero_smul 📖	mathematical	—	GradedMonoid.GSMul.smul GradedMonoid.GMulAction.toGSMul DirectSum.GdistribMulAction.toGMulAction toGdistribMulAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass HVAdd.hVAdd instHVAdd	—	—

GradedModule

Definitions

Name	Category	Theorems
isModule 📖	CompOp	—
linearEquiv 📖	CompOp	—

SetLike

Definitions

Name	Category	Theorems
gdistribMulAction 📖	CompOp	—
gmodule 📖	CompOp	—
gmulAction 📖	CompOp	—

---

← Back to Index