Theorems · Theorem · commutative algebra
ZMod.ker_intCastRingHom
∀ (n : ℕ), RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}The ring homomorphism ℤ → ZMod n has kernel generated by n.
- Defined in
- Mathlib.RingTheory.ZMod
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- RingHomstatement · cited by 10,189
- Idealstatement · cited by 4,748
- ZModstatement and proof · cited by 1,024
- Ideal.spanstatement · cited by 948
- RingHom.kerstatement and proof · cited by 363
- Int.castRingHomstatement and proof · cited by 254
- Ideal.extproof · cited by 131
- Ideal.mem_span_singletonproof · cited by 69
- RingHom.mem_kerproof · cited by 49
- ZMod.intCast_zmod_eq_zero_iff_dvdproof · cited by 14
- Int.coe_castRingHomproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- Int.quotientSpanNatEquivZModproof · cited by 7
- isReduced_zmodproof · cited by 0