Mathlib Map

Theorems · Definition · group theory

MulHom.id

(M : Type u_10) → [inst : Mul M] → M →ₙ* M

The identity map from a type with multiplication to itself.

Defined in
Mathlib.Algebra.Group.Hom.Defs
Cited by
15 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Mul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MulHom.id_apply · cited by 3MulHom.id_applyMulHom.toMulEquiv · cited by 2MulHom.toMulEquivWithOne.mapMulHom_id · cited by 1WithOne.mapMulHom_idMagmaCat.hom_id · cited by 0MagmaCat.hom_idMulHom.comp_id · cited by 0MulHom.comp_idSubsemigroup.map_id · cited by 0Subsemigroup.map_idMagmaCat.ofHom_id · cited by 0MagmaCat.ofHom_idMulHom.toMulEquiv_apply · cited by 0MulHom.toMulEquiv_applyMulHom.id_comp · cited by 0MulHom.id_compMulHom.toMulEquiv_symm_apply · cited by 0MulHom.toMulEquiv_symm_ap…Semigrp.hom_id · cited by 0Semigrp.hom_idNonUnitalRingHom.coe_mulHom_id · cited by 0NonUnitalRingHom.coe_mulH…MulHom.coe_id · cited by 0MulHom.coe_idMonoidAlgebra.mapDomainNonUnitalRingHom_id · cited by 0MonoidAlgebra.mapDomainNo…Semigrp.ofHom_id · cited by 0Semigrp.ofHom_idMulHom · cited by 299MulHomMulHom.idCITED BYCITES

Cites1

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

  • MulHomstatement · cited by 299

Cited by16

Results whose statement or proof uses this declaration.