Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 16:11 2f44ac8f

View on Github →

feat(algebra/monoid_algebra/grading): internal graded structure for an arbitrary degree function (#10435) This gives an internal graded structure of an additive monoid algebra for the grading given by an arbitrary degree function. The grading in the original file is redefined as the grading for the identity degree function.

Estimated changes

Modified src/algebra/monoid_algebra/grading.lean

added def add_monoid_algebra.equiv_grades_by

modified def add_monoid_algebra.grade

added theorem add_monoid_algebra.grade_by.is_internal

added def add_monoid_algebra.grade_by

added theorem add_monoid_algebra.grade_by_id

added theorem add_monoid_algebra.grade_eq_lsingle_range

added theorem add_monoid_algebra.mem_grade_by_iff

added theorem add_monoid_algebra.mem_grade_iff'

added theorem add_monoid_algebra.mem_grade_iff

added def add_monoid_algebra.of_grades_by

added theorem add_monoid_algebra.of_grades_by_comp_to_grades_by

added theorem add_monoid_algebra.of_grades_by_of

added theorem add_monoid_algebra.of_grades_by_to_grades_by

modified theorem add_monoid_algebra.of_grades_comp_to_grades

added theorem add_monoid_algebra.single_mem_grade

added theorem add_monoid_algebra.single_mem_grade_by

modified def add_monoid_algebra.to_grades

added def add_monoid_algebra.to_grades_by

added theorem add_monoid_algebra.to_grades_by_coe

added theorem add_monoid_algebra.to_grades_by_comp_of_grades_by

added theorem add_monoid_algebra.to_grades_by_of_grades_by

added theorem add_monoid_algebra.to_grades_by_single'

added theorem add_monoid_algebra.to_grades_by_single