MixedCharZero

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

Statistics

Metric	Count
Definitions algebraRat, coePNatUnits, pnatCast, MixedCharZero	4
Theorems isUnit_natCast, iff_not_mixedCharZero, nonempty_algebraRat_iff, of_algebraRat, of_not_mixedCharZero, pnatCast_eq_natCast, pnatCast_one, to_not_mixedCharZero, charP_quotient, reduce_to_maximal_ideal, reduce_to_p_prime, toCharZero, isEmpty_algebraRat_iff_mixedCharZero, split_by_characteristic, split_by_characteristic_domain, split_by_characteristic_localRing, split_equalCharZero_mixedCharZero	17
Total	21

EqualCharZero

Definitions

Name	Category	Theorems
algebraRat 📖	CompOp	—
coePNatUnits 📖	CompOp	—
pnatCast 📖	CompOp	2 math math: pnatCast_eq_natCast, pnatCast_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_not_mixedCharZero 📖	mathematical	—	CharZero HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient MixedCharZero	—	to_not_mixedCharZero of_not_mixedCharZero
nonempty_algebraRat_iff 📖	mathematical	—	Algebra Rat.commSemiring CommSemiring.toSemiring CommRing.toCommSemiring CharZero HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient	—	of_algebraRat
of_algebraRat 📖	mathematical	—	CharZero HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient	—	Mathlib.Tactic.Contrapose.contrapose₂ Ideal.eq_top_of_isUnit_mem Ideal.instIsTwoSided_1 map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_natCast IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Nat.cast_injective Rat.instCharZero
of_not_mixedCharZero 📖	mathematical	MixedCharZero	CharZero HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient	—	CharP.exists CharP.charP_to_charZero
pnatCast_eq_natCast 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring pnatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing PNat.val	—	—
pnatCast_one 📖	mathematical	—	pnatCast PNat instOfNatPNatOfNeZeroNat Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instOne	—	Units.ext Units.val_one PNat.isUnit_natCast IsUnit.unit_spec PNat.one_coe Nat.cast_one
to_not_mixedCharZero 📖	mathematical	CharZero HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient	MixedCharZero	—	MixedCharZero.charP_quotient CharP.ofCharZero CharP.eq ne_of_gt

EqualCharZero.PNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_natCast 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing PNat.val	—	Ideal.span_singleton_eq_top not_imp_comm Fact.elim CharZero.cast_injective PNat.ne_zero Ideal.instIsTwoSided_1 map_natCast RingHom.instRingHomClass Nat.cast_zero Ideal.Quotient.eq_zero_iff_mem Ideal.subset_span Set.mem_singleton

MixedCharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charP_quotient 📖	mathematical	—	CharP HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient	—	—
reduce_to_maximal_ideal 📖	mathematical	Nat.Prime	CharP HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient Ideal.IsMaximal	—	Ideal.exists_le_maximal CharP.exists CharP.cast_eq_zero_iff Ideal.instIsTwoSided_1 CharP.cast_eq_zero Nat.Prime.eq_one_or_self_of_dvd CharP.char_ne_one IsDomain.toNontrivial Ideal.Quotient.isDomain Ideal.IsMaximal.isPrime' Ideal.IsMaximal.ne_top
reduce_to_p_prime 📖	—	—	—	—	Nat.Prime.pos charP_quotient Ideal.exists_le_maximal Ideal.instIsTwoSided_1 CharP.cast_eq_zero ne_zero_of_dvd_ne_zero ne_of_gt CharP.cast_eq_zero_iff ringChar.charP map_natCast RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CharP.char_is_prime_or_zero Ideal.Quotient.noZeroDivisors Ideal.IsMaximal.isPrime' IsDomain.toNontrivial Ideal.Quotient.isDomain toCharZero Ideal.IsMaximal.ne_top ringChar.of_eq
toCharZero 📖	mathematical	—	CharZero AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—

(root)

Definitions

Name	Category	Theorems
MixedCharZero 📖	CompData	3 math math: EqualCharZero.to_not_mixedCharZero, isEmpty_algebraRat_iff_mixedCharZero, EqualCharZero.iff_not_mixedCharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmpty_algebraRat_iff_mixedCharZero 📖	mathematical	—	IsEmpty Algebra Rat.commSemiring CommSemiring.toSemiring CommRing.toCommSemiring MixedCharZero	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_and_eq EqualCharZero.iff_not_mixedCharZero EqualCharZero.nonempty_algebraRat_iff
split_by_characteristic 📖	—	—	—	—	CharP.exists split_equalCharZero_mixedCharZero CharP.charP_to_charZero
split_by_characteristic_domain 📖	—	—	—	—	split_by_characteristic CharP.char_is_prime_or_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial
split_by_characteristic_localRing 📖	—	—	—	—	split_by_characteristic charP_zero_or_prime_power
split_equalCharZero_mixedCharZero 📖	—	—	—	—	MixedCharZero.reduce_to_p_prime not_isEmpty_iff isEmpty_algebraRat_iff_mixedCharZero

---

← Back to Index