Quotient

📁 Source: Mathlib/Algebra/CharP/Quotient.lean

Statistics

Metric	Count
Definitions	0
Theorems ker_intAlgebraMap_eq_span, quotient, quotient', quotient_iff, quotient_iff_le_ker_natCast, index_eq_zero, natCast_mem_of_charP_quotient	7
Total	7

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_intAlgebraMap_eq_span 📖	mathematical	—	RingHom.ker RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Int.instCommSemiring Ring.toSemiring RingHom.instFunLike RingHom.instRingHomClass algebraMap Ring.toIntAlgebra Ideal.span Int.instSemiring Set Set.instSingletonSet	—	Ideal.ext RingHom.instRingHomClass eq_intCast intCast_eq_zero_iff
quotient 📖	mathematical	Set Set.instMembership nonunits MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	CharP HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.span Set.instSingletonSet Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1 Ideal.Quotient.eq_zero_iff_mem Ideal.subset_span Set.mem_singleton map_natCast RingHom.instRingHomClass ringChar.of_eq Nat.dvd_prime Fact.out ringChar.dvd isUnit_iff_dvd_one Ideal.mem_span_singleton CharOne.subsingleton
quotient' 📖	mathematical	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CharP HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.instRingQuotient	—	cast_eq_zero_iff Ideal.instIsTwoSided_1 map_natCast RingHom.instRingHomClass Ideal.Quotient.eq sub_zero Ideal.zero_mem
quotient_iff 📖	mathematical	—	CharP HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient AddMonoidWithOne.toNatCast CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	cast_eq_zero_iff Submodule.Quotient.mk_eq_zero quotient'
quotient_iff_le_ker_natCast 📖	mathematical	—	CharP HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient Nat.instSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.comap RingHom Nat.instNonAssocSemiring RingHom.instFunLike Nat.castRingHom RingHom.instRingHomClass RingHom.ker	—	RingHom.instRingHomClass quotient_iff RingHom.ker_eq_comap_bot

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_mem_of_charP_quotient 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	instIsTwoSided_1 Quotient.eq_zero_iff_mem map_natCast RingHom.instRingHomClass CharP.cast_eq_zero

Ideal.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
index_eq_zero 📖	mathematical	—	HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRingQuotient AddSubgroup.index AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing Submodule.toAddSubgroup Semiring.toModule Submodule.Quotient.instZeroQuotient	—	AddSubgroup.index.eq_1 Nat.card_eq Nat.cast_card_eq_zero Nat.cast_zero

---

← Back to Index