Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-08 14:38 13d86df6

View on Github →

chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured G. (#6572) This provides distrib and mul_zero_class for when G is just has_mul, and semigroup for when G is just semigroup. It also weakens the typeclass assumptions on some correspondings lemmas.

Estimated changes

Modified src/algebra/monoid_algebra.lean

modified theorem add_monoid_algebra.lift_nc_smul

modified theorem add_monoid_algebra.mul_apply

modified theorem add_monoid_algebra.mul_apply_antidiagonal

modified theorem add_monoid_algebra.mul_single_apply_aux

modified theorem add_monoid_algebra.mul_single_zero_apply

modified def add_monoid_algebra.of

modified theorem add_monoid_algebra.of_apply

modified theorem add_monoid_algebra.of_injective

modified theorem add_monoid_algebra.single_mul_apply_aux

modified theorem add_monoid_algebra.single_mul_single

modified theorem add_monoid_algebra.single_zero_mul_apply

modified theorem add_monoid_algebra.support_mul

modified theorem monoid_algebra.lift_nc_smul

modified theorem monoid_algebra.map_domain_mul

modified theorem monoid_algebra.mul_apply

modified theorem monoid_algebra.mul_apply_antidiagonal

modified theorem monoid_algebra.mul_single_apply_aux

modified theorem monoid_algebra.mul_single_one_apply

modified theorem monoid_algebra.of_apply

modified theorem monoid_algebra.of_injective

modified theorem monoid_algebra.single_mul_apply_aux

modified theorem monoid_algebra.single_mul_single

modified theorem monoid_algebra.single_one_mul_apply

modified theorem monoid_algebra.single_pow

modified theorem monoid_algebra.support_mul