Theorems · Theorem · group theory
MonoidHom.map_mul
∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N) (a b : M), f (a * b) = f a * f bIf f is a monoid homomorphism then f (a * b) = f a * f b.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 11 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
- MonoidHomstatement and proof · cited by 3,629
- MulOnestatement and proof · cited by 65
- MonoidHom.map_mul'proof · cited by 6
Cited by39
Results whose statement or proof uses this declaration.
- Submonoid.LocalizationMap.lift_eqproof · cited by 11
- CategoryTheory.MonObj.comp_mulproof · cited by 10
- Subgroup.index_comap_of_surjectiveproof · cited by 5
- Submonoid.LocalizationMap.eq_of_eqproof · cited by 5
- LinearMap.det_compproof · cited by 4
- QuotientGroup.kerLift_injectiveproof · cited by 3
- Submonoid.LocalizationMap.mul_invproof · cited by 3
- Subgroup.leftTransversals.diff_mul_diffproof · cited by 3
- Con.comapQuotientEquivOfSurjstatement · cited by 3
- Sylow.normalizer_sup_eq_topproof · cited by 2
- MonoidHom.ext_intproof · cited by 2