Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-17 23:24 e83458cb

View on Github →

feat(algebra/group_power): Add mul/add variants of powers_hom and friends (#4636)

Estimated changes

Modified src/algebra/group_power/lemmas.lean

added def gmultiples_add_hom

added theorem gmultiples_add_hom_apply

added theorem gmultiples_add_hom_symm_apply

added def gpowers_mul_hom

added theorem gpowers_mul_hom_apply

added theorem gpowers_mul_hom_symm_apply

added def multiples_add_hom

added theorem multiples_add_hom_apply

added theorem multiples_add_hom_symm_apply

added def powers_mul_hom

added theorem powers_mul_hom_apply

added theorem powers_mul_hom_symm_apply