Mathlib v3 is deprecated. Go to Mathlib v4

Def smul_add_hom

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 View on Github →