Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-02 19:54 2594f48f

View on Github →

style(linear_algebra/tensor_product): renaming and changing some proofs

Estimated changes

Modified group_theory/free_abelian_group.lean

added theorem free_abelian_group.to_add_comm_group.coe

added theorem free_abelian_group.to_add_comm_group.sub

Modified linear_algebra/tensor_product.lean

modified theorem is_bilinear_map.comm

modified theorem is_bilinear_map.comp

added theorem is_bilinear_map.linear_left

deleted theorem is_bilinear_map.linear_pair

added theorem is_bilinear_map.linear_right

added theorem is_bilinear_map.neg_left

deleted theorem is_bilinear_map.neg_pair

added theorem is_bilinear_map.neg_right

deleted theorem is_bilinear_map.pair_linear

deleted theorem is_bilinear_map.pair_neg

deleted theorem is_bilinear_map.pair_zero

added theorem is_bilinear_map.zero_left

deleted theorem is_bilinear_map.zero_pair

added theorem is_bilinear_map.zero_right

modified structure is_bilinear_map

modified theorem tensor_product.add_of

added theorem tensor_product.of.add_left

added theorem tensor_product.of.add_right

added theorem tensor_product.of.smul

modified theorem tensor_product.of_add

modified theorem tensor_product.of_smul

added theorem tensor_product.smul.is_add_group_hom

deleted def tensor_product.smul.is_add_group_hom

modified theorem tensor_product.smul_of

modified def tensor_product