Mathlib Map

Theorems · Definition · group theory

MulHom.fst

(M : Type u_3) → (N : Type u_4) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M

Given magmas M, N, the natural projection homomorphism from M × N to M.

Defined in
Mathlib.Algebra.Group.Prod
Cited by
8 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
MulMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NonUnitalRingHom.fst · cited by 8NonUnitalRingHom.fstMulHom.prodMap · cited by 4MulHom.prodMapMulHom.coprod · cited by 2MulHom.coprodSubsemigroup.srange_fst · cited by 1Subsemigroup.srange_fstMulHom.prod_unique · cited by 0MulHom.prod_uniqueMulHom.coe_fst · cited by 0MulHom.coe_fstSubsemigroup.le_prod_iff · cited by 0Subsemigroup.le_prod_iffMulHom.fst_comp_prod · cited by 0MulHom.fst_comp_prodSubsemigroup.prod_eq_top_iff · cited by 0Subsemigroup.prod_eq_top_…Subsemigroup.prod_top · cited by 0Subsemigroup.prod_topMulHom.prodMap_def · cited by 0MulHom.prodMap_defMulHom · cited by 299MulHomMulHom.fstCITED 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 by11

Results whose statement or proof uses this declaration.