Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smul_add_hom_apply

Modification history

2020-04-26 03:56
src/algebra/module.lean
chore(algebra/module): use bundled homs for `smul_sum` and `sum_smul` (#2529)
Added smul_add_hom_applyView on Github →