Theorems · Definition · commutative algebra
Int.quotientSpanEquivZMod
(a : ℤ) → ℤ ⧸ Ideal.span {a} ≃+* ZMod a.natAbsℤ modulo the ideal generated by a : ℤ is ZMod a.natAbs.
- Defined in
- Mathlib.Data.ZMod.QuotientRing
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 90 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
- Int.quotientSpanNatEquivZModproof · cited by 7
- Int.span_natAbsproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- AddCommGroup.equiv_free_prod_directSum_zmodproof · cited by 2
- Submodule.quotientEquivPiZModproof · cited by 2
- Module.finite_of_fg_torsionproof · cited by 1
- Int.quotientSpanEquivZMod_comp_Quotient_mkstatement · cited by 0
- Int.quotientSpanEquivZMod_comp_castRingHomstatement and proof · cited by 0