Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-16 23:59 efa6877b

View on Github →

feat(algebra/category/Module): the free/forgetful adjunction for R-modules (#6168)

Estimated changes

Created src/algebra/category/Module/adjunctions.lean

added def Module.adj

added def Module.free

Modified src/data/equiv/mul_add.lean

added def mul_equiv.arrow_congr

added def mul_equiv.monoid_hom_congr

Modified src/data/finsupp/basic.lean

added theorem finsupp.induction_linear

added theorem finsupp.sum_map_domain_index_add_monoid_hom

Modified src/linear_algebra/basic.lean

added def linear_map.ring_lmap_equiv_self

Modified src/linear_algebra/finsupp.lean

added theorem finsupp.lift_apply

added theorem finsupp.lift_symm_apply