Theorems · Theorem · group theory
MonoidHom.map_pow
∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (a : M) (n : ℕ), f (a ^ n) = f a ^ n- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- map_powproof · cited by 503
Cited by30
Results whose statement or proof uses this declaration.
- norm_powproof · cited by 106
- abs_powproof · cited by 36
- orderOf_injectiveproof · cited by 12
- ENNReal.toReal_powproof · cited by 9
- AbsoluteValue.map_powproof · cited by 8
- nnnorm_powproof · cited by 8
- Matrix.det_powproof · cited by 7
- Monoid.extproof · cited by 7
- Polynomial.pow_compproof · cited by 7
- MonoidHom.isOfFinOrderproof · cited by 6
- smul_pow'proof · cited by 5
- AddChar.map_nsmul_eq_powproof · cited by 5