Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-03 00:10 0df6f778

View on Github →

style(linear_algebra/tensor_product): rename of -> tmul and ⊗ₛ -> ⊗ₜ; some cleanup in free_abelian_group

Estimated changes

Modified group_theory/free_abelian_group.lean

deleted def free_abelian_group.UMP

deleted theorem free_abelian_group.coe_def

added def free_abelian_group.to_add_comm_group.UMP

deleted theorem free_abelian_group.to_add_comm_group.add

deleted theorem free_abelian_group.to_add_comm_group.coe

deleted theorem free_abelian_group.to_add_comm_group.ext

deleted def free_abelian_group.to_add_comm_group.is_add_group_hom

deleted theorem free_abelian_group.to_add_comm_group.neg

deleted theorem free_abelian_group.to_add_comm_group.of

deleted theorem free_abelian_group.to_add_comm_group.sub

deleted theorem free_abelian_group.to_add_comm_group.unique

deleted theorem free_abelian_group.to_add_comm_group.zero

modified def free_abelian_group.to_add_comm_group

Modified linear_algebra/tensor_product.lean

deleted theorem tensor_product.add_of

added theorem tensor_product.add_tmul

modified theorem tensor_product.bilinear

deleted theorem tensor_product.of.add_left

deleted theorem tensor_product.of.add_right

deleted theorem tensor_product.of.smul

deleted def tensor_product.of

deleted theorem tensor_product.of_add

deleted theorem tensor_product.of_smul

deleted theorem tensor_product.smul_of

added theorem tensor_product.smul_tmul

added theorem tensor_product.tmul.add_left

added theorem tensor_product.tmul.add_right

added theorem tensor_product.tmul.smul

added def tensor_product.tmul

added theorem tensor_product.tmul_add

added theorem tensor_product.tmul_smul

deleted theorem tensor_product.to_module.of

added theorem tensor_product.to_module.tmul