Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-26 03:56 ee6f20a6

View on Github →

chore(algebra/module): use bundled homs for smul_sum and sum_smul (#2529)

Estimated changes

Modified src/algebra/group/hom.lean

added def monoid_hom.flip

added theorem monoid_hom.flip_apply

added theorem monoid_hom.inv_apply

added theorem monoid_hom.mul_apply

added theorem monoid_hom.one_apply

Modified src/algebra/module.lean

added def smul_add_hom

added theorem smul_add_hom_apply

Modified src/group_theory/group_action.lean

added def const_smul_hom

added theorem const_smul_hom_apply

Modified src/ring_theory/noetherian.lean