Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-18 23:02 f52d2cc2

View on Github →

chore(group_theory/free_abelian_group, abelianization): rename to_comm_group, to_add_comm_group -> lift

Estimated changes

Modified group_theory/abelianization.lean

added theorem abelianization.lift.of

added theorem abelianization.lift.unique

added def abelianization.lift

deleted def abelianization.to_comm_group.is_group_hom

deleted theorem abelianization.to_comm_group.of

deleted theorem abelianization.to_comm_group.unique

deleted def abelianization.to_comm_group

Modified group_theory/free_abelian_group.lean

added theorem free_abelian_group.lift.map_hom

added def free_abelian_group.lift.universal

added def free_abelian_group.lift

deleted def free_abelian_group.to_add_comm_group.UMP

deleted def free_abelian_group.to_add_comm_group

Modified group_theory/subgroup.lean

added theorem group.closure_subset_iff

Modified linear_algebra/tensor_product.lean