Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-17 12:38 36e01274

View on Github →

feat(linear_algebra/basic): add_monoid_hom_lequiv_int (#7629) From LTE.

Estimated changes

Modified src/algebra/module/basic.lean

added theorem add_monoid_hom.map_nat_module_smul

Modified src/algebra/module/linear_map.lean

added def add_monoid_hom.to_nat_linear_map

Modified src/linear_algebra/basic.lean

added def add_monoid_hom_lequiv_int

added def add_monoid_hom_lequiv_nat