Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 13:15 03b88c14

View on Github →

feat(algebra/category/Module): Free R C, the free R-linear completion of a category (#7177) The free R-linear completion of a category.

Estimated changes

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

added def category_theory.Free.embedding

added def category_theory.Free.embedding_lift_iso

added def category_theory.Free.ext

added def category_theory.Free.lift

added theorem category_theory.Free.lift_map_single

added def category_theory.Free.lift_unique

added def category_theory.Free.of

added theorem category_theory.Free.single_comp_single

added def category_theory.Free

Modified src/category_theory/preadditive/additive_functor.lean

added theorem category_theory.functor.map_gsmul

Modified src/category_theory/preadditive/default.lean

added theorem category_theory.preadditive.comp_gsmul

added theorem category_theory.preadditive.gsmul_comp

Modified src/linear_algebra/tensor_product.lean