Mathlib Changelog
Changelog
About
Github
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