Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 20:25 f7795d1a

View on Github →

feat(monoid_algebra/grading): add_monoid_algebras permit an internal grading (#8927)

Estimated changes

Created src/algebra/monoid_algebra/grading.lean

added def add_monoid_algebra.equiv_grades

added theorem add_monoid_algebra.grade.is_internal

added def add_monoid_algebra.grade

added def add_monoid_algebra.of_grades

added theorem add_monoid_algebra.of_grades_comp_to_grades

added theorem add_monoid_algebra.of_grades_of

added theorem add_monoid_algebra.of_grades_to_grades

added def add_monoid_algebra.to_grades

added theorem add_monoid_algebra.to_grades_coe

added theorem add_monoid_algebra.to_grades_comp_of_grades

added theorem add_monoid_algebra.to_grades_of_grades

added theorem add_monoid_algebra.to_grades_single