Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-02 19:54 4b5ad0ea

View on Github →

feat(linear_algebra,group_theory): add tensor product and supporting material

Estimated changes

Modified algebra/group.lean

Modified algebra/ring.lean

Created group_theory/abelianization.lean

added def abelianization.of

added def abelianization.to_comm_group.is_group_hom

added theorem abelianization.to_comm_group.of

added theorem abelianization.to_comm_group.unique

added def abelianization.to_comm_group

added def abelianization

added def commutator

Modified group_theory/coset.lean

added theorem quotient_group.induction_on'

added theorem quotient_group.induction_on

Created group_theory/free_abelian_group.lean

added def free_abelian_group.UMP

added theorem free_abelian_group.coe_def

added def free_abelian_group.of

added theorem free_abelian_group.to_add_comm_group.add

added theorem free_abelian_group.to_add_comm_group.ext

added def free_abelian_group.to_add_comm_group.is_add_group_hom

added theorem free_abelian_group.to_add_comm_group.neg

added theorem free_abelian_group.to_add_comm_group.of

added theorem free_abelian_group.to_add_comm_group.unique

added theorem free_abelian_group.to_add_comm_group.zero

added def free_abelian_group.to_add_comm_group

added def free_abelian_group

Modified group_theory/quotient_group.lean

Modified group_theory/subgroup.lean

Created linear_algebra/tensor_product.lean

added theorem is_bilinear_map.comm

added theorem is_bilinear_map.comp

added theorem is_bilinear_map.linear_pair

added theorem is_bilinear_map.neg_pair

added theorem is_bilinear_map.pair_linear

added theorem is_bilinear_map.pair_neg

added theorem is_bilinear_map.pair_zero

added theorem is_bilinear_map.zero_pair

added structure is_bilinear_map

added theorem tensor_product.add_of

added theorem tensor_product.bilinear

added def tensor_product.of

added theorem tensor_product.of_add

added theorem tensor_product.of_smul

added def tensor_product.relators

added def tensor_product.smul.aux

added def tensor_product.smul.is_add_group_hom

added def tensor_product.smul

added theorem tensor_product.smul_of

added theorem tensor_product.to_module.add

added def tensor_product.to_module.equiv

added theorem tensor_product.to_module.ext

added def tensor_product.to_module.linear

added theorem tensor_product.to_module.of

added theorem tensor_product.to_module.smul

added theorem tensor_product.to_module.unique

added def tensor_product.to_module

added def tensor_product