Commit 2023-05-28 20:07 6936ba2b

View on Github →

feat: port Algebra.MonoidAlgebra.Grading (#4450)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/Grading.lean

added theorem AddMonoidAlgebra.GradesBy.decompose_single

added def AddMonoidAlgebra.decomposeAux

added theorem AddMonoidAlgebra.decomposeAux_coe

added theorem AddMonoidAlgebra.decomposeAux_eq_decompose

added theorem AddMonoidAlgebra.decomposeAux_single

added theorem AddMonoidAlgebra.grade.decompose_single

added theorem AddMonoidAlgebra.grade.isInternal

added theorem AddMonoidAlgebra.gradeBy.isInternal

added theorem AddMonoidAlgebra.gradeBy_id

added theorem AddMonoidAlgebra.grade_eq_lsingle_range

added theorem AddMonoidAlgebra.mem_gradeBy_iff

added theorem AddMonoidAlgebra.mem_grade_iff'

added theorem AddMonoidAlgebra.mem_grade_iff

added theorem AddMonoidAlgebra.single_mem_grade

added theorem AddMonoidAlgebra.single_mem_gradeBy