Documentation Verification Report

GradedMulAction

📁 Source: Mathlib/Algebra/GradedMulAction.lean

Statistics

Metric	Count
Definitions `toGMulAction`, `toGSMul`, `GMulAction`, `toGSMul`, `toMulAction`, `GSMul`, `smul`, `toSMul`, `GradedSMul`, `toGSMul`	10
Theorems `mul_smul`, `one_smul`, `mk_smul_mk`, `toGradedSMul`, `smul_mem`, `graded_smul`, `coe_GSMul`	7
Total	17

GradedMonoid

Definitions

Name	Category	Theorems
`GMulAction` 📖	CompData	—
`GSMul` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_smul_mk` 📖	mathematical	—	`GradedMonoid` `GSMul.toSMul` `HVAdd.hVAdd` `instHVAdd` `GSMul.smul`	—	—

GradedMonoid.GMonoid

Definitions

Name	Category	Theorems
`toGMulAction` 📖	CompOp	—

GradedMonoid.GMul

Definitions

Name	Category	Theorems
`toGSMul` 📖	CompOp	—

GradedMonoid.GMulAction

Definitions

Name	Category	Theorems
`toGSMul` 📖	CompOp	9 math math: `DirectSum.Gmodule.smulAddMonoidHom_apply_of_of`, `DirectSum.Gmodule.of_smul_of`, `DirectSum.GdistribMulAction.smul_zero`, `mul_smul`, `DirectSum.Gmodule.zero_smul`, `one_smul`, `DirectSum.gsmulHom_apply_apply`, `DirectSum.GdistribMulAction.smul_add`, `DirectSum.Gmodule.add_smul`
`toMulAction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_smul` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GSMul.toSMul` `toGSMul` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMonoid.toGMul`	—	—
`one_smul` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GSMul.toSMul` `toGSMul` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `GradedMonoid.GMonoid.toGOne`	—	—

GradedMonoid.GSMul

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	9 math math: `DirectSum.Gmodule.smulAddMonoidHom_apply_of_of`, `DirectSum.Gmodule.of_smul_of`, `DirectSum.GdistribMulAction.smul_zero`, `DirectSum.Gmodule.zero_smul`, `SetLike.coe_GSMul`, `GradedMonoid.mk_smul_mk`, `DirectSum.gsmulHom_apply_apply`, `DirectSum.GdistribMulAction.smul_add`, `DirectSum.Gmodule.add_smul`
`toSMul` 📖	CompOp	3 math math: `GradedMonoid.GMulAction.mul_smul`, `GradedMonoid.GMulAction.one_smul`, `GradedMonoid.mk_smul_mk`

SetLike

Definitions

Name	Category	Theorems
`GradedSMul` 📖	CompData	2 math math: `GradedMul.toGradedSMul`, `IsModuleFiltration.toGradedSMul`
`toGSMul` 📖	CompOp	1 math math: `coe_GSMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_GSMul` 📖	mathematical	—	`instMembership` `HVAdd.hVAdd` `instHVAdd` `GradedMonoid.GSMul.smul` `toGSMul`	—	—

SetLike.GradedMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toGradedSMul` 📖	mathematical	—	`SetLike.GradedSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`mul_mem` `SetLike.GradedMonoid.toGradedMul`

SetLike.GradedSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_mem` 📖	mathematical	`SetLike.instMembership`	`HVAdd.hVAdd` `instHVAdd`	—	—

SetLike.IsHomogeneousElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`graded_smul` 📖	—	`SetLike.IsHomogeneousElem`	—	—	`SetLike.GradedSMul.smul_mem`

---

← Back to Index