Commit 2021-12-14 11:07 9078914e

View on Github →

feat(algebra/group): make map_[z]pow generic in monoid_hom_class (#10749) This PR makes map_pow take a monoid_hom_class instead of specifically a monoid_hom.

Estimated changes

Modified src/algebra/group/hom.lean

added theorem map_pow

added theorem map_zpow'

added theorem map_zpow

deleted theorem monoid_hom.map_pow

deleted theorem monoid_hom.map_zpow'

deleted theorem monoid_hom.map_zpow

Modified src/algebra/group_power/basic.lean

deleted theorem ring_hom.map_pow

Modified src/category_theory/preadditive/default.lean

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/eval.lean

deleted theorem polynomial.map_pow

Modified src/data/polynomial/lifts.lean

Modified src/field_theory/abel_ruffini.lean

Modified src/field_theory/finite/basic.lean

Modified src/field_theory/finite/galois_field.lean

Modified src/linear_algebra/tensor_product.lean

deleted theorem tensor_product.map_pow

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/dickson.lean

Modified src/ring_theory/polynomial/vieta.lean

Modified src/ring_theory/power_series/well_known.lean

Modified src/ring_theory/roots_of_unity.lean