Commit 2020-10-16 03:25 cc14658a

View on Github →

chore(algebra/group_powers): Add missing lemmas (#4635) This part of the file defines four equivalences, but goes on to state lemmas about only one of them. This provides the lemmas for the other three.

Estimated changes

Modified src/algebra/group_power/lemmas.lean

added theorem add_monoid_hom.apply_int

added theorem add_monoid_hom.apply_nat

added theorem gmultiples_hom_apply

added theorem gmultiples_hom_symm_apply

added theorem gpowers_hom_apply

added theorem gpowers_hom_symm_apply

deleted theorem mnat_monoid_hom_eq

deleted theorem mnat_monoid_hom_ext

added theorem monoid_hom.apply_mint

added theorem monoid_hom.apply_mnat

added theorem monoid_hom.ext_mint

added theorem monoid_hom.ext_mnat

added theorem multiples_hom_apply

added theorem multiples_hom_symm_apply