Theorems · Definition · order theory
Setoid.ker
{α : Type u_1} → {β : Type u_2} → (α → β) → Setoid αThe kernel of a function is an equivalence relation.
- Defined in
- Mathlib.Data.Setoid.Basic
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.onFunproof · cited by 570
Cited by71
Results whose statement or proof uses this declaration.
- HomogeneousLocalizationproof · cited by 69
- Con.kerproof · cited by 24
- AddCon.kerproof · cited by 24
- DoubleCoset.setoidproof · cited by 13
- Setoid.kerLiftstatement · cited by 9
- HomogeneousLocalization.val_mulproof · cited by 9
- Topology.IsQuotientMap.liftproof · cited by 6
- SimpleGraph.Coloring.colorClassesproof · cited by 6
- Topology.IsEmbedding.isStrictMap_iffproof · cited by 6
- Topology.IsQuotientMap.homeomorphstatement and proof · cited by 5
- Setoid.ker_eq_lift_of_injectivestatement and proof · cited by 4
- HomogeneousLocalization.val_addproof · cited by 4