Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-09 13:50 66a86ffe

View on Github →

refactor(*): rename is_group_hom.mul to map_mul (#911)

refactor(*): rename is_group_hom.mul to map_mul
Fix splits_mul

Estimated changes

Modified src/algebra/big_operators.lean

added theorem is_group_anti_hom.map_prod

deleted theorem is_group_anti_hom.prod

added theorem is_group_hom.map_multiset_prod

added theorem is_group_hom.map_prod

deleted theorem is_group_hom.multiset_prod

deleted theorem is_group_hom.prod

Modified src/algebra/direct_sum.lean

Modified src/algebra/group.lean

added theorem is_add_group_hom.map_sub

modified theorem is_add_group_hom.sub

deleted theorem is_add_group_hom_sub

deleted theorem is_group_anti_hom.inv

added theorem is_group_anti_hom.map_inv

added theorem is_group_anti_hom.map_one

deleted theorem is_group_anti_hom.one

modified theorem is_group_hom.inv

added theorem is_group_hom.map_inv

added theorem is_group_hom.map_one

added theorem is_group_hom.mul

deleted theorem is_group_hom.one

deleted theorem is_group_hom_inv

deleted theorem is_group_hom_mul

Modified src/algebra/group_power.lean

modified theorem is_add_group_hom.gsmul

added theorem is_add_group_hom.map_gsmul

added theorem is_add_group_hom.map_smul

deleted theorem is_add_group_hom.smul

deleted theorem is_add_group_hom_gsmul

deleted theorem is_group_hom.gpow

added theorem is_group_hom.map_gpow

added theorem is_group_hom.map_pow

deleted theorem is_group_hom.pow

Modified src/analysis/complex/exponential.lean

modified theorem real.angle.coe_gsmul

Modified src/field_theory/splitting_field.lean

Modified src/group_theory/abelianization.lean

Modified src/group_theory/free_abelian_group.lean

Modified src/group_theory/free_group.lean

Modified src/group_theory/group_action.lean

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/quotient_group.lean

Modified src/group_theory/subgroup.lean

Modified src/linear_algebra/tensor_product.lean

Modified src/ring_theory/localization.lean

Modified src/topology/algebra/group_completion.lean

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/algebra/uniform_ring.lean