Mathlib Map

Theorems · Definition · group theory

MulHom.toFun

{M : Type u_10} → {N : Type u_11} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → M → N

The underlying function

Defined in
Mathlib.Algebra.Group.Hom.Defs
Cited by
36 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
MulMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MonoidHomClass.toMonoidHom · cited by 294MonoidHomClass.toMonoidHomSubmonoid.LocalizationMap.toMonoidHom · cited by 33LocalizationMap.toMonoidH…MonoidAlgebra.of · cited by 30MonoidAlgebra.ofCon.mk' · cited by 22Con.mk'NonUnitalAlgHom.comp · cited by 21NonUnitalAlgHom.compAddMonoidAlgebra.of · cited by 19AddMonoidAlgebra.ofSet.singletonMonoidHom · cited by 6Set.singletonMonoidHomSubmonoid.LocalizationMap.isLocalizationMap · cited by 5LocalizationMap.isLocaliz…MulRingNorm.mulRingNormEquivAbsoluteValue · cited by 4MulRingNorm.mulRingNormEq…NonUnitalAlgHom.restrictScalars · cited by 4NonUnitalAlgHom.restrictS…Filter.pureMonoidHom · cited by 3Filter.pureMonoidHomPi.evalNonUnitalStarAlgHom · cited by 3Pi.evalNonUnitalStarAlgHomNonUnitalRingHom.toAddMonoidHom · cited by 3NonUnitalRingHom.toAddMon…NonUnitalAlgHom.codRestrict · cited by 3NonUnitalAlgHom.codRestri…Finset.singletonMonoidHom · cited by 3Finset.singletonMonoidHomMulHom · cited by 299MulHomMulHom.toFunCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • MulHomstatement and proof · cited by 299

Cited by80

Results whose statement or proof uses this declaration.