Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.to_add_monoid_hom_injective

Modification history

2020-10-26 18:39
src/algebra/module/basic.lean
chore(algebra/module,linear_algebra): split off a `linear_map` file (#4476) …
Modified linear_map.to_add_monoid_hom_injectiveView on Github →
2020-10-08 15:41
src/algebra/module/basic.lean
chore(*): add a few more `unique` instances (#4511) …
Modified linear_map.to_add_monoid_hom_injectiveView on Github →
2020-10-06 10:22
src/algebra/module/basic.lean
feat(data/finsupp): lift a collection of `add_monoid_hom`s to an `add_monoid_hom` on `α →₀ β` (#4395)
Added linear_map.to_add_monoid_hom_injectiveView on Github →