Commit 2022-05-04 07:50 85657f1b

View on Github →

feat(algebra/category/FinVect): has finite limits (#13793)

Estimated changes

Modified src/algebra/category/FinVect.lean

added def FinVect.of

Created src/algebra/category/FinVect/limits.lean

added def FinVect.forget₂_creates_limit

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

added theorem Module.pi_iso_pi_hom_ker_subtype

added theorem Module.pi_iso_pi_inv_kernel_ι

added def Module.product_cone

added def Module.product_cone_is_limit

Modified src/category_theory/concrete_category/basic.lean

Modified src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

added def category_theory.limits.colimit_cocone_of_coequalizer_and_coproduct

added def category_theory.limits.colimit_quotient_coproduct

added def category_theory.limits.limit_cone_of_equalizer_and_product

added def category_theory.limits.limit_subobject_product

Modified src/linear_algebra/finite_dimensional.lean