Commit 2020-10-29 13:24 8b858d0b

View on Github →

feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid (#3490) The extra _s required to make this still build are unfortunate, but hopefully someone else can work out how to remove them in a later PR.

Estimated changes

Modified src/algebra/direct_limit.lean

Modified src/algebra/direct_sum.lean

added theorem direct_sum.add_apply

added theorem direct_sum.zero_apply

Modified src/algebra/lie/basic.lean

modified theorem lie_algebra.of_associative_algebra_hom_id

Modified src/data/dfinsupp.lean

modified theorem dfinsupp.ext

modified theorem dfinsupp.smul_apply

modified theorem dfinsupp.support_smul

modified def dfinsupp.to_has_scalar

modified def dfinsupp.to_semimodule

Modified src/linear_algebra/direct_sum_module.lean

added theorem direct_sum.smul_apply

added theorem direct_sum.support_smul