Theorems · Definition · commutative algebra
RingCon.ker
{M : Type u_1} → {N : Type u_2} → [inst : NonAssocSemiring M] → [inst_1 : NonAssocSemiring N] → (M →+* N) → RingCon MThe kernel of a ring homomorphism as a ring congruence relation.
- Defined in
- Mathlib.RingTheory.Congruence.Hom
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHomstatement and proof · cited by 10,189
- Bot.botproof · cited by 4,720
- NonAssocSemiringstatement and proof · cited by 805
- RingConstatement · cited by 219
- RingCon.comapproof · cited by 32
Cited by60
Results whose statement or proof uses this declaration.
- RingCon.liftstatement and proof · cited by 16
- RingCon.liftₐstatement and proof · cited by 12
- SymmetricAlgebra.liftproof · cited by 9
- SymmetricAlgebra.lift_ι_applyproof · cited by 8
- RingCon.kerLiftstatement and proof · cited by 5
- RingCon.quotientKerEquivRangeₐstatement and proof · cited by 4
- RingCon.kerLiftₐstatement and proof · cited by 3
- RingCon.quotientQuotientEquivQuotientstatement · cited by 3
- RingCon.quotientQuotientEquivQuotientₐstatement and proof · cited by 3
- RingCon.liftₐEquivstatement and proof · cited by 2
- PolynomialLaw.toFun'_eq_of_diagramproof · cited by 2
- RingCon.rangeS_liftstatement and proof · cited by 2