Documentation Verification Report

QuotientRing

📁 Source: Mathlib/Data/ZMod/QuotientRing.lean

Statistics

Metric	Count
Definitions `quotientSpanEquivZMod`, `quotientSpanNatEquivZMod`, `equivPi`, `prodEquivPi`	4
Theorems `quotientSpanEquivZMod_comp_Quotient_mk`, `quotientSpanEquivZMod_comp_castRingHom`, `quotientSpanNatEquivZMod_comp_Quotient_mk`, `quotientSpanNatEquivZMod_comp_castRingHom`	4
Total	8

Int

Definitions

Name	Category	Theorems
`quotientSpanEquivZMod` 📖	CompOp	2 math math: `quotientSpanEquivZMod_comp_Quotient_mk`, `quotientSpanEquivZMod_comp_castRingHom`
`quotientSpanNatEquivZMod` 📖	CompOp	3 math math: `quotientSpanNatEquivZMod_comp_Quotient_mk`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `quotientSpanNatEquivZMod_comp_castRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotientSpanEquivZMod_comp_Quotient_mk` 📖	mathematical	—	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instCommRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `ZMod` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `ZMod.commRing` `RingHomClass.toRingHom` `RingEquiv` `instSemiring` `Ideal.instHasQuotient_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `quotientSpanEquivZMod` `castRingHom`	—	`Ideal.instIsTwoSided_1` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`quotientSpanEquivZMod_comp_castRingHom` 📖	mathematical	—	`RingHom.comp` `ZMod` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instCommRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `instSemiring` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `ZMod.commRing` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHomClass.toRingHom` `RingEquiv` `Ideal.instHasQuotient_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.symm` `quotientSpanEquivZMod` `castRingHom`	—	`RingHom.ext` `Ideal.instIsTwoSided_1` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `eq_intCast` `RingHom.instRingHomClass`
`quotientSpanNatEquivZMod_comp_Quotient_mk` 📖	mathematical	—	`RingHom.comp` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instCommRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `ZMod` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `ZMod.commRing` `RingHomClass.toRingHom` `RingEquiv` `instSemiring` `Ideal.instHasQuotient_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `quotientSpanNatEquivZMod` `castRingHom`	—	`Ideal.instIsTwoSided_1` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`quotientSpanNatEquivZMod_comp_castRingHom` 📖	mathematical	—	`RingHom.comp` `ZMod` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instCommRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `instSemiring` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `ZMod.commRing` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHomClass.toRingHom` `RingEquiv` `Ideal.instHasQuotient_1` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.symm` `quotientSpanNatEquivZMod` `castRingHom`	—	`RingHom.ext` `Ideal.instIsTwoSided_1` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `eq_intCast` `RingHom.instRingHomClass`

ZMod

Definitions

Name	Category	Theorems
`equivPi` 📖	CompOp	—
`prodEquivPi` 📖	CompOp	—

---

← Back to Index