Documentation Verification Report

Grading

📁 Source: Mathlib/Algebra/MonoidAlgebra/Grading.lean

Statistics

Metric	Count
Definitions `decomposeAux`, `grade`, `gradedAlgebra`, `gradeBy`, `gradedAlgebra`	5
Theorems `decompose_single`, `decomposeAux_coe`, `decomposeAux_eq_decompose`, `decomposeAux_single`, `decompose_single`, `gradedMonoid`, `isInternal`, `gradedMonoid`, `isInternal`, `gradeBy_id`, `grade_eq_lsingle_range`, `mem_gradeBy_iff`, `mem_grade_iff`, `mem_grade_iff'`, `single_mem_grade`, `single_mem_gradeBy`	16
Total	21

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`decomposeAux` 📖	CompOp	3 math math: `decomposeAux_coe`, `decomposeAux_single`, `decomposeAux_eq_decompose`
`grade` 📖	CompOp	8 math math: `grade_eq_lsingle_range`, `gradeBy_id`, `mem_grade_iff'`, `single_mem_grade`, `mem_grade_iff`, `grade.decompose_single`, `grade.isInternal`, `grade.gradedMonoid`
`gradeBy` 📖	CompOp	9 math math: `decomposeAux_coe`, `gradeBy.isInternal`, `gradeBy_id`, `GradesBy.decompose_single`, `gradeBy.gradedMonoid`, `decomposeAux_single`, `decomposeAux_eq_decompose`, `single_mem_gradeBy`, `mem_gradeBy_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decomposeAux_coe` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DirectSum` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `gradeBy` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `Submodule.addCommMonoid` `semiring` `DirectSum.semiring` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `gradeBy.gradedMonoid` `algebra` `Algebra.id` `DirectSum.instAlgebra` `Submodule.module` `Submodule.galgebra` `AlgHom.funLike` `decomposeAux` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `DirectSum.of`	—	`Submodule.addSubmonoidClass` `gradeBy.gradedMonoid` `Finsupp.induction` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `Finsupp.support_single_ne_zero` `Set.union_subset_iff` `Finset.coe_union` `Finsupp.support_add_eq` `mem_gradeBy_iff` `Set.singleton_subset_iff` `Finset.coe_singleton` `SetLike.GradedMonoid.toGradedMul` `single_mem_gradeBy` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `decomposeAux_single` `AddMonoidHomClass.toAddHomClass` `DirectSum.of_eq_of_gradedMonoid_eq`
`decomposeAux_eq_decompose` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DirectSum` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `gradeBy` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `Submodule.addCommMonoid` `semiring` `DirectSum.semiring` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `gradeBy.gradedMonoid` `algebra` `Algebra.id` `DirectSum.instAlgebra` `Submodule.module` `Submodule.galgebra` `AlgHom.funLike` `decomposeAux` `Equiv` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition` `gradeBy.gradedAlgebra`	—	`Submodule.addSubmonoidClass` `gradeBy.gradedMonoid`
`decomposeAux_single` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DirectSum` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `gradeBy` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `Submodule.addCommMonoid` `semiring` `DirectSum.semiring` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `gradeBy.gradedMonoid` `algebra` `Algebra.id` `DirectSum.instAlgebra` `Submodule.module` `Submodule.galgebra` `AlgHom.funLike` `decomposeAux` `Finsupp.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `DirectSum.of` `single_mem_gradeBy`	—	`gradeBy.gradedMonoid` `single_mem_gradeBy` `lift_single` `DirectSum.of_smul` `DirectSum.of_eq_of_gradedMonoid_eq` `Sigma.subtype_ext` `smul_single'` `mul_one`
`gradeBy_id` 📖	mathematical	—	`gradeBy` `grade`	—	—
`grade_eq_lsingle_range` 📖	mathematical	—	`grade` `LinearMap.range` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finsupp.instAddCommMonoid` `Semiring.toModule` `Finsupp.module` `RingHom.id` `RingHomSurjective.ids` `Finsupp.lsingle`	—	`Submodule.ext` `RingHomSurjective.ids` `mem_grade_iff'`
`mem_gradeBy_iff` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `gradeBy` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Set.preimage` `Set.instSingletonSet`	—	—
`mem_grade_iff` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `grade` `Finset` `Finset.instHasSubset` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.instSingleton`	—	`Finset.coe_subset` `Finset.coe_singleton`
`mem_grade_iff'` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `grade` `LinearMap.range` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.id` `RingHomSurjective.ids` `Finsupp.lsingle`	—	`RingHomSurjective.ids` `mem_grade_iff` `Finsupp.support_subset_singleton'`
`single_mem_grade` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `grade` `single`	—	`single_mem_gradeBy`
`single_mem_gradeBy` 📖	mathematical	—	`AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `gradeBy` `single`	—	`Finset.mem_singleton` `Finsupp.support_single_subset`

AddMonoidAlgebra.GradesBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decompose_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DirectSum` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `AddMonoidAlgebra.gradeBy` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition` `AddMonoidAlgebra.semiring` `AddMonoidAlgebra.gradeBy.gradedAlgebra` `Finsupp.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `DirectSum.of` `AddMonoidAlgebra.single_mem_gradeBy`	—	`AddMonoidAlgebra.decomposeAux_single`

AddMonoidAlgebra.grade

Definitions

Name	Category	Theorems
`gradedAlgebra` 📖	CompOp	1 math math: `decompose_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decompose_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidAlgebra` `CommSemiring.toSemiring` `DirectSum` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `AddMonoidAlgebra.grade` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition` `AddMonoidAlgebra.semiring` `gradedAlgebra` `Finsupp.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidHom` `Submodule.addCommMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.of` `AddMonoidAlgebra.single_mem_grade`	—	`AddMonoidAlgebra.decomposeAux_single`
`gradedMonoid` 📖	mathematical	—	`SetLike.GradedMonoid` `AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `Submodule.setLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring` `AddMonoidAlgebra.grade`	—	`AddMonoidAlgebra.gradeBy.gradedMonoid`
`isInternal` 📖	mathematical	—	`DirectSum.IsInternal` `AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `Submodule.setLike` `Submodule.addSubmonoidClass` `AddMonoidAlgebra.grade`	—	`DirectSum.Decomposition.isInternal` `Submodule.addSubmonoidClass`

AddMonoidAlgebra.gradeBy

Definitions

Name	Category	Theorems
`gradedAlgebra` 📖	CompOp	2 math math: `AddMonoidAlgebra.GradesBy.decompose_single`, `AddMonoidAlgebra.decomposeAux_eq_decompose`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gradedMonoid` 📖	mathematical	—	`SetLike.GradedMonoid` `AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `Submodule.setLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring` `AddMonoidAlgebra.gradeBy` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `Finset.mem_singleton` `Finsupp.support_single_subset` `AddMonoidAlgebra.one_def` `Finset.mem_add` `AddMonoidAlgebra.support_mul` `map_add` `AddMonoidHomClass.toAddHomClass`
`isInternal` 📖	mathematical	—	`DirectSum.IsInternal` `AddMonoidAlgebra` `CommSemiring.toSemiring` `Submodule` `AddMonoidAlgebra.addAddCommMonoid` `AddMonoidAlgebra.module` `Semiring.toModule` `Submodule.setLike` `Submodule.addSubmonoidClass` `AddMonoidAlgebra.gradeBy` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	—	`DirectSum.Decomposition.isInternal` `Submodule.addSubmonoidClass`

---

← Back to Index