MixedCharZero

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

Statistics

Metric	Count
Definitions MixedCharZero	1
Theorems iff_not_mixedCharZero, nonempty_algebraRat_iff, 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	11
Total	12

EqualCharZero

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	—	—
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	—	—

MixedCharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charP_quotient 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring CharP HasQuotient.Quotient Ideal.instHasQuotient_1 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient	—	—
reduce_to_maximal_ideal 📖	mathematical	Nat.Prime	Ideal CommSemiring.toSemiring CommRing.toCommSemiring CharP HasQuotient.Quotient 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	2 math math: 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