ZMod

📁 Source: Mathlib/RingTheory/ZMod.lean

Statistics

Metric	Count
Definitions	0
Theorems ker_intCastRingHom, ringHom_eq_of_ker_eq, instIsReducedZModOfFactSquarefreeNat, isReduced_zmod	4
Total	4

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_intCastRingHom 📖	mathematical	—	RingHom.ker ZMod RingHom Semiring.toNonAssocSemiring Int.instSemiring NonAssocRing.toNonAssocSemiring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing commRing CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.instRingHomClass Int.castRingHom Ideal.span Set Set.instSingletonSet	—	Ideal.ext RingHom.instRingHomClass Ideal.mem_span_singleton RingHom.mem_ker Int.coe_castRingHom intCast_zmod_eq_zero_iff_dvd
ringHom_eq_of_ker_eq 📖	—	RingHom.ker ZMod RingHom Semiring.toNonAssocSemiring Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring commRing RingHom.instFunLike RingHom.instRingHomClass	—	—	RingHom.instRingHomClass ringHom_rightInverse le_of_eq RingHom.liftOfRightInverse_comp RingHom.ext_zmod RingHom.id_comp

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsReducedZModOfFactSquarefreeNat 📖	mathematical	—	IsReduced ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	isReduced_zmod Fact.out
isReduced_zmod 📖	mathematical	—	IsReduced ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Squarefree Nat.instMonoid	—	RingHom.instRingHomClass RingHom.ker_isRadical_iff_reduced_of_surjective ZMod.ringHom_surjective ZMod.ker_intCastRingHom isRadical_iff_span_singleton isRadical_iff_squarefree_or_zero Int.instIsCancelMulZero instDecompositionMonoidOfNonemptyGCDMonoid IsBezout.nonemptyGCDMonoid IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain Int.instIsDomain Int.squarefree_natCast Nat.cast_eq_zero Int.instCharZero

---

← Back to Index