Documentation Verification Report

GradedMonoid

📁 Source: Mathlib/Algebra/GradedMonoid.lean

Statistics

Metric	Count
Definitions `gCommMonoid`, `GradedMonoid`, `GCommMonoid`, `toCommMonoid`, `toGMonoid`, `GMonoid`, `gnpow`, `gnpowRec`, `toGMul`, `toGOne`, `toMonoid`, `GMul`, `mul`, `toMul`, `GOne`, `one`, `toOne`, `commMonoid`, `monoid`, `mul`, `mulAction`, `one`, `smul`, `instInhabitedOfDefault`, `instMulAction`, `instNatPowOfNat`, `instSMul`, `mk`, `mkZeroMonoidHom`, `tacticApply_gmonoid_gnpowRec_succ_tac`, `tacticApply_gmonoid_gnpowRec_zero_tac`, `dProd`, `dProdIndex`, `gMonoid`, `gMul`, `gOne`, `instCommMonoid`, `instMonoid`, `submonoid`, `GradedMonoid`, `GradedMul`, `GradedOne`, `IsHomogeneousElem`, `gCommMonoid`, `gMonoid`, `gMul`, `gOne`, `homogeneousSubmonoid`	48
Theorems `mul_comm`, `gnpowRec_succ`, `gnpowRec_zero`, `gnpow_succ'`, `gnpow_zero'`, `mul_assoc`, `mul_one`, `one_mul`, `smul_eq_mul`, `fst_mul`, `fst_one`, `fst_pow`, `fst_smul`, `instIsScalarTower`, `instSMulCommClass`, `list_prod_map_eq_dProd`, `list_prod_ofFn_eq_dProd`, `mk_list_dProd`, `mk_mul_mk`, `mk_pow`, `mk_zero_pow`, `mk_zero_smul`, `smul_mk`, `snd_mul`, `snd_one`, `snd_pow`, `snd_smul`, `dProdIndex_cons`, `dProdIndex_eq_map_sum`, `dProdIndex_nil`, `dProd_cons`, `dProd_monoid`, `dProd_nil`, `gMonoid_gnpow`, `gMul_mul`, `gOne_one`, `coe_mul`, `coe_one`, `coe_pow`, `coe_submonoid`, `toGradedMul`, `toGradedOne`, `mul_mem`, `one_mem`, `mul`, `coe_gMul`, `coe_gOne`, `coe_gnpow`, `coe_list_dProd`, `isHomogeneousElem_coe`, `isHomogeneousElem_one`, `list_dProd_eq`, `list_prod_map_mem_graded`, `list_prod_ofFn_mem_graded`, `mul_mem_graded`, `one_mem_graded`, `pow_mem_graded`, `prod_mem_graded`, `prod_pow_mem_graded`	59
Total	107

CommMonoid

Definitions

Name	Category	Theorems
`gCommMonoid` 📖	CompOp	—

GradedMonoid

Definitions

Name	Category	Theorems
`GCommMonoid` 📖	CompData	—
`GMonoid` 📖	CompData	—
`GMul` 📖	CompData	—
`GOne` 📖	CompData	—
`instInhabitedOfDefault` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instNatPowOfNat` 📖	CompOp	1 math math: `mk_zero_pow`
`instSMul` 📖	CompOp	8 math math: `instIsScalarTower`, `smul_mk`, `fst_smul`, `instSMulCommClass`, `smulCommClass_right`, `DirectSum.GAlgebra.smul_def`, `isScalarTower_right`, `snd_smul`
`mk` 📖	CompOp	—
`mkZeroMonoidHom` 📖	CompOp	—
`tacticApply_gmonoid_gnpowRec_succ_tac` 📖	CompOp	—
`tacticApply_gmonoid_gnpowRec_zero_tac` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_mul` 📖	mathematical	—	`GradedMonoid` `GMul.toMul`	—	—
`fst_one` 📖	mathematical	—	`GradedMonoid` `GOne.toOne`	—	—
`fst_pow` 📖	mathematical	—	`GradedMonoid` `Monoid.toNatPow` `GMonoid.toMonoid` `AddMonoid.toNatSMul`	—	—
`fst_smul` 📖	mathematical	—	`GradedMonoid` `instSMul`	—	—
`instIsScalarTower` 📖	mathematical	`IsScalarTower`	`GradedMonoid` `instSMul`	—	`smul_assoc`
`instSMulCommClass` 📖	mathematical	`SMulCommClass`	`GradedMonoid` `instSMul`	—	`SMulCommClass.smul_comm`
`list_prod_map_eq_dProd` 📖	mathematical	—	`GradedMonoid` `GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GMonoid.toGMul` `GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `GMonoid.toGOne` `List.dProdIndex` `List.dProd`	—	`mk_list_dProd` `Sigma.eta`
`list_prod_ofFn_eq_dProd` 📖	mathematical	—	`GradedMonoid` `GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GMonoid.toGMul` `GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `GMonoid.toGOne` `List.dProdIndex` `List.dProd`	—	`List.ofFn_eq_map` `list_prod_map_eq_dProd`
`mk_list_dProd` 📖	mathematical	—	`List.dProdIndex` `List.dProd` `GradedMonoid` `GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GMonoid.toGMul` `GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `GMonoid.toGOne`	—	—
`mk_mul_mk` 📖	mathematical	—	`GradedMonoid` `GMul.toMul` `GMul.mul`	—	—
`mk_pow` 📖	mathematical	—	`GradedMonoid` `Monoid.toNatPow` `GMonoid.toMonoid` `AddMonoid.toNatSMul` `GMonoid.gnpow`	—	—
`mk_zero_pow` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instNatPowOfNat` `GradedMonoid` `Monoid.toNatPow` `GMonoid.toMonoid`	—	`nsmul_zero`
`mk_zero_smul` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `GradeZero.smul` `GradedMonoid` `GMul.toMul` `AddZero.toAdd`	—	`zero_add`
`smul_mk` 📖	mathematical	—	`GradedMonoid` `instSMul`	—	—
`snd_mul` 📖	mathematical	—	`GradedMonoid` `GMul.toMul` `GMul.mul`	—	—
`snd_one` 📖	mathematical	—	`GradedMonoid` `GOne.toOne` `GOne.one`	—	—
`snd_pow` 📖	mathematical	—	`GradedMonoid` `Monoid.toNatPow` `GMonoid.toMonoid` `GMonoid.gnpow`	—	—
`snd_smul` 📖	mathematical	—	`GradedMonoid` `instSMul`	—	—

GradedMonoid.GCommMonoid

Definitions

Name	Category	Theorems
`toCommMonoid` 📖	CompOp	—
`toGMonoid` 📖	CompOp	1 math math: `mul_comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_comm` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `GradedMonoid.GMonoid.toGMul` `AddCommMonoid.toAddMonoid` `toGMonoid`	—	—

GradedMonoid.GMonoid

Definitions

Name	Category	Theorems
`gnpow` 📖	CompOp	7 math math: `Monoid.gMonoid_gnpow`, `GradedMonoid.mk_pow`, `DirectSum.ofPow`, `gnpow_zero'`, `SetLike.coe_gnpow`, `gnpow_succ'`, `GradedMonoid.snd_pow`
`gnpowRec` 📖	CompOp	2 math math: `gnpowRec_zero`, `gnpowRec_succ`
`toGMul` 📖	CompOp	10 math math: `GradedMonoid.mk_list_dProd`, `mul_one`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `GradedMonoid.GMulAction.mul_smul`, `mul_assoc`, `List.dProd_cons`, `one_mul`, `GradedMonoid.list_prod_map_eq_dProd`, `gnpow_succ'`, `GradedMonoid.GCommMonoid.mul_comm`
`toGOne` 📖	CompOp	15 math math: `GradedMonoid.mk_list_dProd`, `mul_one`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `gnpow_zero'`, `TensorProduct.algebraMap_gradedMul`, `List.dProd_nil`, `one_mul`, `GradedMonoid.list_prod_map_eq_dProd`, `TensorProduct.gradedMul_algebraMap`, `DirectSum.liftRingHom_symm_apply_coe`, `DirectSum.ofList_dProd`, `DirectSum.GAlgebra.map_one`, `DirectSum.list_prod_ofFn_of_eq_dProd`, `DirectSum.liftRingHom_apply`, `GradedMonoid.GMulAction.one_smul`
`toMonoid` 📖	CompOp	6 math math: `GradedMonoid.mk_zero_pow`, `GradedMonoid.mk_pow`, `GradedMonoid.smulCommClass_right`, `GradedMonoid.fst_pow`, `GradedMonoid.isScalarTower_right`, `GradedMonoid.snd_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gnpowRec_succ` 📖	mathematical	—	`AddMonoid.toNatSMul` `gnpowRec` `GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`succ_nsmul`
`gnpowRec_zero` 📖	mathematical	—	`AddMonoid.toNatSMul` `gnpowRec` `GradedMonoid` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`zero_nsmul`
`gnpow_succ'` 📖	mathematical	—	`AddMonoid.toNatSMul` `gnpow` `GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `toGMul`	—	—
`gnpow_zero'` 📖	mathematical	—	`AddMonoid.toNatSMul` `gnpow` `GradedMonoid` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toGOne`	—	—
`mul_assoc` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `toGMul`	—	—
`mul_one` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `toGMul` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toGOne`	—	—
`one_mul` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `toGMul` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toGOne`	—	—

GradedMonoid.GMul

Definitions

Name	Category	Theorems
`mul` 📖	CompOp	28 math math: `DirectSum.mulHom_of_of`, `GradedMonoid.mk_mul_mk`, `TensorPower.gMul_eq_coe_linearMap`, `DirectSum.gMulHom_apply_apply`, `TensorPower.algebraMap₀_mul`, `TensorPower.mul_assoc`, `DirectSum.of_mul_of`, `DirectSum.GNonUnitalNonAssocSemiring.mul_zero`, `TensorPower.tprod_mul_tprod`, `DirectSum.decompose_mul_add_left`, `TensorPower.mul_one`, `SetLike.coe_gMul`, `TensorPower.toTensorAlgebra_gMul`, `DirectSum.GNonUnitalNonAssocSemiring.add_mul`, `DirectSum.GAlgebra.map_mul`, `TensorPower.algebraMap₀_mul_algebraMap₀`, `TensorPower.gMul_def`, `List.dProd_cons`, `GradedMonoid.snd_mul`, `TensorPower.one_mul`, `DirectSum.mul_eq_sum_support_ghas_mul`, `DirectSum.mul_eq_dfinsuppSum`, `TensorPower.mul_algebraMap₀`, `DirectSum.GNonUnitalNonAssocSemiring.zero_mul`, `DirectSum.decompose_mul_add_right`, `Mul.gMul_mul`, `DirectSum.GNonUnitalNonAssocSemiring.mul_add`, `DirectSum.gMulLHom_apply_apply`
`toMul` 📖	CompOp	23 math math: `GradedMonoid.mk_mul_mk`, `DirectSum.GSemiring.gnpow_succ'`, `GradedMonoid.mk_list_dProd`, `GradedMonoid.GMonoid.mul_one`, `DirectSum.GSemiring.mul_assoc`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `GradedMonoid.mk_zero_smul`, `GradedMonoid.GMulAction.mul_smul`, `GradedMonoid.GMonoid.gnpowRec_succ`, `DirectSum.GCommRing.mul_comm`, `DirectSum.GSemiring.one_mul`, `GradedMonoid.GMonoid.mul_assoc`, `TensorPower.list_prod_gradedMonoid_mk_single`, `GradedMonoid.GMonoid.one_mul`, `GradedMonoid.list_prod_map_eq_dProd`, `GradedMonoid.fst_mul`, `GradedMonoid.snd_mul`, `DirectSum.GCommSemiring.mul_comm`, `DirectSum.GAlgebra.smul_def`, `DirectSum.GAlgebra.commutes`, `GradedMonoid.GMonoid.gnpow_succ'`, `DirectSum.GSemiring.mul_one`, `GradedMonoid.GCommMonoid.mul_comm`

GradedMonoid.GOne

Definitions

Name	Category	Theorems
`one` 📖	CompOp	15 math math: `GradedMonoid.snd_one`, `DirectSum.one_def`, `TensorPower.algebraMap₀_one`, `One.gOne_one`, `TensorPower.algebraMap₀_eq_smul_one`, `TensorPower.mul_one`, `SetLike.coe_gOne`, `TensorPower.toTensorAlgebra_gOne`, `List.dProd_nil`, `TensorPower.gOne_def`, `TensorPower.one_mul`, `DirectSum.liftRingHom_symm_apply_coe`, `DirectSum.GAlgebra.map_one`, `DirectSum.GSemiring.natCast_succ`, `DirectSum.liftRingHom_apply`
`toOne` 📖	CompOp	14 math math: `GradedMonoid.mk_list_dProd`, `GradedMonoid.GMonoid.mul_one`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `GradedMonoid.snd_one`, `GradedMonoid.GMonoid.gnpow_zero'`, `GradedMonoid.fst_one`, `GradedMonoid.GMonoid.gnpowRec_zero`, `DirectSum.GSemiring.gnpow_zero'`, `DirectSum.GSemiring.one_mul`, `TensorPower.list_prod_gradedMonoid_mk_single`, `GradedMonoid.GMonoid.one_mul`, `GradedMonoid.list_prod_map_eq_dProd`, `GradedMonoid.GMulAction.one_smul`, `DirectSum.GSemiring.mul_one`

GradedMonoid.GradeZero

Definitions

Name	Category	Theorems
`commMonoid` 📖	CompOp	—
`monoid` 📖	CompOp	1 math math: `DirectSum.of_zero_pow`
`mul` 📖	CompOp	2 math math: `smul_eq_mul`, `DirectSum.of_zero_mul`
`mulAction` 📖	CompOp	—
`one` 📖	CompOp	1 math math: `DirectSum.of_zero_one`
`smul` 📖	CompOp	3 math math: `smul_eq_mul`, `DirectSum.of_zero_smul`, `GradedMonoid.mk_zero_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_eq_mul` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `smul` `mul`	—	—

List

Definitions

Name	Category	Theorems
`dProd` 📖	CompOp	10 math math: `GradedMonoid.mk_list_dProd`, `SetLike.coe_list_dProd`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `SetLike.list_dProd_eq`, `dProd_nil`, `dProd_cons`, `GradedMonoid.list_prod_map_eq_dProd`, `DirectSum.ofList_dProd`, `DirectSum.list_prod_ofFn_of_eq_dProd`, `dProd_monoid`
`dProdIndex` 📖	CompOp	11 math math: `GradedMonoid.mk_list_dProd`, `SetLike.coe_list_dProd`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `SetLike.list_dProd_eq`, `dProdIndex_nil`, `dProdIndex_cons`, `dProdIndex_eq_map_sum`, `dProd_cons`, `GradedMonoid.list_prod_map_eq_dProd`, `DirectSum.ofList_dProd`, `DirectSum.list_prod_ofFn_of_eq_dProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dProdIndex_cons` 📖	mathematical	—	`dProdIndex` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`dProdIndex_eq_map_sum` 📖	mathematical	—	`dProdIndex` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`dProdIndex_nil` 📖	mathematical	—	`dProdIndex` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`dProd_cons` 📖	mathematical	—	`dProd` `GradedMonoid.GMul.mul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMonoid.toGMul` `dProdIndex`	—	—
`dProd_monoid` 📖	mathematical	—	`dProd` `Monoid.gMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`dProd_nil` `dProd_cons`
`dProd_nil` 📖	mathematical	—	`dProd` `GradedMonoid.GOne.one` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `GradedMonoid.GMonoid.toGOne`	—	—

Monoid

Definitions

Name	Category	Theorems
`gMonoid` 📖	CompOp	2 math math: `gMonoid_gnpow`, `List.dProd_monoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gMonoid_gnpow` 📖	mathematical	—	`GradedMonoid.GMonoid.gnpow` `gMonoid` `toNatPow`	—	—

Mul

Definitions

Name	Category	Theorems
`gMul` 📖	CompOp	1 math math: `gMul_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gMul_mul` 📖	mathematical	—	`GradedMonoid.GMul.mul` `gMul`	—	—

One

Definitions

Name	Category	Theorems
`gOne` 📖	CompOp	3 math math: `DirectSum.toAddMonoidAlgebra_one`, `gOne_one`, `AddMonoidAlgebra.toDirectSum_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gOne_one` 📖	mathematical	—	`GradedMonoid.GOne.one` `gOne`	—	—

SetLike

Definitions

Name	Category	Theorems
`GradedMonoid` 📖	CompData	10 math math: `GradedRing.toGradedMonoid`, `CliffordAlgebra.evenOdd.gradedMonoid`, `MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring`, `ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower`, `AddMonoidAlgebra.gradeBy.gradedMonoid`, `Submodule.nat_power_gradedMonoid`, `IsRingFiltration.toGradedMonoid`, `MvPolynomial.HomogeneousSubmodule.gradedMonoid`, `AddMonoidAlgebra.grade.gradedMonoid`, `MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid`
`GradedMul` 📖	CompData	1 math math: `GradedMonoid.toGradedMul`
`GradedOne` 📖	CompData	1 math math: `GradedMonoid.toGradedOne`
`IsHomogeneousElem` 📖	MathDef	4 math math: `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous`, `homogeneous_zero_submodule`, `isHomogeneousElem_coe`, `isHomogeneousElem_one`
`gCommMonoid` 📖	CompOp	—
`gMonoid` 📖	CompOp	3 math math: `coe_list_dProd`, `list_dProd_eq`, `coe_gnpow`
`gMul` 📖	CompOp	3 math math: `DirectSum.decompose_mul_add_left`, `coe_gMul`, `DirectSum.decompose_mul_add_right`
`gOne` 📖	CompOp	5 math math: `DirectSum.decompose_symm_one`, `listProd_apply_eq_zero'`, `coe_gOne`, `listProd_apply_eq_zero`, `DirectSum.decompose_one`
`homogeneousSubmonoid` 📖	CompOp	1 math math: `Ideal.IsHomogeneous.iff_exists`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_gMul` 📖	mathematical	—	`instMembership` `GradedMonoid.GMul.mul` `gMul`	—	—
`coe_gOne` 📖	mathematical	—	`instMembership` `GradedMonoid.GOne.one` `gOne`	—	—
`coe_gnpow` 📖	mathematical	—	`instMembership` `AddMonoid.toNatSMul` `GradedMonoid.GMonoid.gnpow` `gMonoid` `Monoid.toNatPow`	—	—
`coe_list_dProd` 📖	mathematical	—	`instMembership` `List.dProdIndex` `List.dProd` `gMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`List.dProd_nil` `GradedMonoid.toGradedOne` `coe_gOne` `List.dProd_cons` `GradedMonoid.toGradedMul` `coe_gMul`
`isHomogeneousElem_coe` 📖	mathematical	—	`IsHomogeneousElem` `instMembership`	—	`Subtype.prop`
`isHomogeneousElem_one` 📖	mathematical	—	`IsHomogeneousElem`	—	`one_mem_graded`
`list_dProd_eq` 📖	mathematical	—	`List.dProd` `instMembership` `gMonoid` `List.dProdIndex` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `list_prod_map_mem_graded` `Subtype.prop` `List.dProdIndex_eq_map_sum`	—	`list_prod_map_mem_graded` `Subtype.prop` `List.dProdIndex_eq_map_sum` `coe_list_dProd`
`list_prod_map_mem_graded` 📖	mathematical	`instMembership`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`one_mem_graded` `GradedMonoid.toGradedOne` `mul_mem_graded` `GradedMonoid.toGradedMul`
`list_prod_ofFn_mem_graded` 📖	mathematical	`instMembership`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`List.ofFn_eq_map` `list_prod_map_mem_graded`
`mul_mem_graded` 📖	—	`instMembership`	—	—	`GradedMul.mul_mem`
`one_mem_graded` 📖	mathematical	—	`instMembership`	—	`GradedOne.one_mem`
`pow_mem_graded` 📖	mathematical	`instMembership`	`AddMonoid.toNatSMul` `Monoid.toNatPow`	—	`pow_zero` `zero_nsmul` `one_mem_graded` `GradedMonoid.toGradedOne` `pow_succ'` `succ_nsmul'` `mul_mem_graded` `GradedMonoid.toGradedMul`
`prod_mem_graded` 📖	mathematical	`instMembership`	`Finset.sum` `Finset.prod`	—	`Finset.induction_on` `GradedMonoid.toGradedOne` `Finset.prod_insert` `Finset.sum_insert` `mul_mem_graded` `GradedMonoid.toGradedMul`
`prod_pow_mem_graded` 📖	mathematical	`instMembership`	`Finset.sum` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Finset.prod` `Monoid.toNatPow` `CommMonoid.toMonoid`	—	`prod_mem_graded` `pow_mem_graded`

SetLike.GradeZero

Definitions

Name	Category	Theorems
`instCommMonoid` 📖	CompOp	—
`instMonoid` 📖	CompOp	4 math math: `coe_pow`, `coe_mul`, `AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective`, `coe_one`
`submonoid` 📖	CompOp	1 math math: `coe_submonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mul` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`coe_one` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`coe_pow` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Monoid.toNatPow` `instMonoid`	—	—
`coe_submonoid` 📖	mathematical	—	`SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `Submonoid.instSetLike` `submonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

SetLike.GradedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toGradedMul` 📖	mathematical	—	`SetLike.GradedMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`toGradedOne` 📖	mathematical	—	`SetLike.GradedOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

SetLike.GradedMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_mem` 📖	—	`SetLike.instMembership`	—	—	—

SetLike.GradedOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_mem` 📖	mathematical	—	`SetLike.instMembership`	—	—

SetLike.IsHomogeneousElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul` 📖	—	`SetLike.IsHomogeneousElem`	—	—	`SetLike.mul_mem_graded`

(root)

Definitions

Name	Category	Theorems
`GradedMonoid` 📖	CompOp	41 math math: `GradedMonoid.mk_mul_mk`, `DirectSum.GSemiring.gnpow_succ'`, `GradedMonoid.mk_list_dProd`, `GradedMonoid.mk_zero_pow`, `GradedMonoid.mk_pow`, `GradedMonoid.GMonoid.mul_one`, `DirectSum.GSemiring.mul_assoc`, `GradedMonoid.instIsScalarTower`, `GradedMonoid.list_prod_ofFn_eq_dProd`, `GradedMonoid.snd_one`, `GradedMonoid.smul_mk`, `GradedMonoid.GMonoid.gnpow_zero'`, `GradedMonoid.fst_smul`, `GradedMonoid.fst_one`, `GradedMonoid.instSMulCommClass`, `GradedMonoid.GMonoid.gnpowRec_zero`, `GradedMonoid.mk_zero_smul`, `GradedMonoid.smulCommClass_right`, `GradedMonoid.fst_pow`, `GradedMonoid.GMulAction.mul_smul`, `GradedMonoid.GMonoid.gnpowRec_succ`, `DirectSum.GCommRing.mul_comm`, `DirectSum.GSemiring.gnpow_zero'`, `DirectSum.GSemiring.one_mul`, `GradedMonoid.GMonoid.mul_assoc`, `TensorPower.list_prod_gradedMonoid_mk_single`, `GradedMonoid.GMonoid.one_mul`, `GradedMonoid.list_prod_map_eq_dProd`, `GradedMonoid.fst_mul`, `GradedMonoid.snd_mul`, `DirectSum.GCommSemiring.mul_comm`, `DirectSum.GAlgebra.smul_def`, `DirectSum.GAlgebra.commutes`, `GradedMonoid.GMonoid.gnpow_succ'`, `GradedMonoid.isScalarTower_right`, `GradedMonoid.GMulAction.one_smul`, `GradedMonoid.mk_smul_mk`, `DirectSum.GSemiring.mul_one`, `GradedMonoid.snd_pow`, `GradedMonoid.GCommMonoid.mul_comm`, `GradedMonoid.snd_smul`

---

← Back to Index