Theorems · Definition · commutative algebra
Int.quotientSpanNatEquivZMod
(n : ℕ) → ℤ ⧸ Ideal.span {↑n} ≃+* ZMod nℤ modulo the ideal generated by n : ℕ is ZMod n.
- Defined in
- Mathlib.Data.ZMod.QuotientRing
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Idealstatement · cited by 4,748
- HasQuotient.Quotientstatement · cited by 2,301
- RingEquivstatement · cited by 1,147
- ZModstatement · cited by 1,024
- Ideal.spanstatement · cited by 948
- RingEquiv.symmproof · cited by 567
- RingEquiv.transproof · cited by 54
- Ideal.quotEquivOfEqproof · cited by 15
- RingHom.quotientKerEquivOfRightInverseproof · cited by 3
- ZMod.ker_intCastRingHomproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- Int.quotientSpanEquivZModproof · cited by 4
- Int.quotientSpanNatEquivZMod_comp_castRingHomstatement and proof · cited by 3
- NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_spanproof · cited by 2
- RingOfIntegers.ZModXQuotSpanEquivQuotSpanproof · cited by 2
- ZMod.prodEquivPiproof · cited by 1
- NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_applystatement · cited by 0
- Int.quotientSpanNatEquivZMod_comp_Quotient_mkstatement · cited by 0
- RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_applyproof · cited by 0