Theorems · Theorem · commutative algebra
RingHom.mem_ker
∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
[rcf : RingHomClass F R S] {f : F} {r : R}, r ∈ RingHom.ker f ↔ f r = 0An element is in the kernel if and only if it maps to zero.
- Defined in
- Mathlib.RingTheory.Ideal.Maps
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
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
- Semiringstatement and proof · cited by 13,802
- Idealstatement and proof · cited by 4,748
- FunLikestatement and proof · cited by 2,560
- RingHom.kerstatement · cited by 363
- RingHomClassstatement and proof · cited by 193
- Submodule.mem_botproof · cited by 55
- Ideal.mem_comapproof · cited by 54
Cited by49
Results whose statement or proof uses this declaration.
- Ideal.ker_le_comapproof · cited by 8
- Algebra.Generators.Cotangent.exactproof · cited by 6
- Algebra.Presentation.aeval_val_relationproof · cited by 5
- IsLocalization.away_of_isIdempotentElemproof · cited by 4
- AlgebraicGeometry.Scheme.Hom.range_subset_ker_supportproof · cited by 4
- Ideal.ker_quotient_liftproof · cited by 4
- PadicInt.zmod_cast_comp_toZModPowproof · cited by 4
- Module.End.isSemisimple_of_squarefree_aeval_eq_zeroproof · cited by 4
- IsLocalRing.residue_eq_zero_iffproof · cited by 4
- MvPolynomial.ker_mapproof · cited by 3
- Ideal.map_sInfproof · cited by 3
- PadicInt.ker_toZModPowproof · cited by 3