Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-24 00:26 1a341fd8

View on Github →

feat(algebra/*): Tensor product is the fibered coproduct in CommRing (#9338)

Estimated changes

Created src/algebra/category/CommRing/pushout.lean

added def CommRing.pushout_cocone

added theorem CommRing.pushout_cocone_X

added theorem CommRing.pushout_cocone_inl

added theorem CommRing.pushout_cocone_inr

added def CommRing.pushout_cocone_is_colimit

Modified src/ring_theory/tensor_product.lean

added def algebra.tensor_product.lmul'

added theorem algebra.tensor_product.lmul'_apply_tmul

added theorem algebra.tensor_product.lmul'_comp_include_left

added theorem algebra.tensor_product.lmul'_comp_include_right

added theorem algebra.tensor_product.lmul'_to_linear_map

added theorem algebra.tensor_product.map_comp_include_left

added theorem algebra.tensor_product.map_comp_include_right

added def algebra.tensor_product.product_map

added theorem algebra.tensor_product.product_map_apply_tmul

added theorem algebra.tensor_product.product_map_left

added theorem algebra.tensor_product.product_map_left_apply

added theorem algebra.tensor_product.product_map_right

added theorem algebra.tensor_product.product_map_right_apply