Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.smul_mk

Modification history

2021-04-02 21:56
src/algebra/module/prod.lean
refactor(algebra/add_torsor): use `to_additive` for `add_action` (#6914)
Modified prod.smul_mkView on Github →
2021-02-08 10:21
src/algebra/module/prod.lean
chore(algebra/module/prod): add missing instances (#6055) …
Modified prod.smul_mkView on Github →
2020-07-23 18:29
src/algebra/module/prod.lean
refactor(algebra/pi_instance): delete pi_instance file, and move instances to group/ring etc appropriately (#3513)
Modified prod.smul_mkView on Github →
2018-11-05 10:47
algebra/pi_instances.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Added prod.smul_mkView on Github →