Theorem zero_smul
Modification history
2021-03-27 03:05
src/algebra/smul_with_zero.lean
chore(algebra/smul_with_zero): add missing injective / surjective transferring functions (#6892)
Modified zero_smulView on Github →2021-03-15 09:03
src/algebra/module/basic.lean
feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introduce `mul_action_with_zero` and `M`-regular elements (#6590) …
Modified zero_smulView on Github →2020-04-13 05:19
src/algebra/module.lean
chore(algebra/module): rename type vars, minor cleanup, add module docstring (#2392) …
Modified zero_smulView on Github →2020-04-11 04:27
src/algebra/module.lean
chore(*): switch to lean 3.8.0 (#2361) …
Modified zero_smulView on Github →2018-11-05 10:47
algebra/module.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Modified zero_smulView on Github →