Theorems · Theorem · group theory

Con.mapOfSurjective_eq_mapGen

∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] {c : Con M} {f : F} (h : Con.ker f ≤ c) (hf : Function.Surjective ⇑f),
  Con.mapGen ⇑f = Con.mapOfSurjective f h hf

A specialization of 'the smallest congruence relation containing a congruence relation c equals c'.

Defined in: Mathlib.GroupTheory.Congruence.Hom
Cited by: 0 results in Mathlib
Foundations: Depth 36 from the axioms · uses propext, Quot.sound
Assumes: Mul Mul FunLike MulHomClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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

DFunLike.coestatement and proof · cited by 62,936
FunLikestatement and proof · cited by 2,560
Constatement and proof · cited by 152
MulHomClassstatement and proof · cited by 73
Con.kerstatement and proof · cited by 24
Con.mapGenstatement and proof · cited by 1
Con.mapOfSurjectivestatement and proof · cited by 1
Con.conGen_of_conproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.