CharAndCard

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

Statistics

Metric	Count
Definitions	0
Theorems charP_of_card_eq_prime, charP_of_card_eq_prime_pow, isUnit_iff_not_dvd_char, isUnit_iff_not_dvd_char_of_ringChar_ne_zero, not_isUnit_prime_of_dvd_card, prime_dvd_char_iff_dvd_card	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charP_of_card_eq_prime 📖	mathematical	Fintype.card	CharP AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	Fintype.one_lt_card_iff_nontrivial Nat.Prime.one_lt Fact.out CharP.charP_iff_prime_eq_zero Nat.cast_card_eq_zero
charP_of_card_eq_prime_pow 📖	mathematical	Fintype.card Monoid.toNatPow Nat.instMonoid	CharP AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	not_subsingleton IsDomain.toNontrivial Fintype.card_le_one_iff_subsingleton pow_zero Eq.le CharP.charP_iff_prime_eq_zero Fact.out Nat.cast_pow isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors Nat.cast_card_eq_zero
isUnit_iff_not_dvd_char 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ringChar Semiring.toNonAssocSemiring	—	isUnit_iff_not_dvd_char_of_ringChar_ne_zero CharP.char_ne_zero_of_finite ringChar.charP
isUnit_iff_not_dvd_char_of_ringChar_ne_zero 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ringChar Semiring.toNonAssocSemiring	—	CharP.cast_eq_zero ringChar.charP Fact.out IsUnit.exists_left_inv Nat.Prime.not_dvd_one mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero mul_one mul_assoc mul_comm CharP.intCast_eq_zero_iff Nat.cast_zero Int.cast_zero Int.cast_natCast one_mul MulZeroClass.mul_zero Nat.cast_mul Nat.Coprime.isCoprime Nat.Prime.coprime_iff_not_dvd IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid add_zero Int.cast_add Int.cast_mul Int.cast_one
not_isUnit_prime_of_dvd_card 📖	mathematical	Fintype.card	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	isUnit_iff_not_dvd_char Finite.of_fintype prime_dvd_char_iff_dvd_card
prime_dvd_char_iff_dvd_card 📖	mathematical	—	ringChar Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Fintype.card	—	Dvd.dvd.trans CharP.intCast_eq_zero_iff ringChar.charP Nat.cast_zero Int.cast_zero Int.cast_natCast Nat.cast_card_eq_zero exists_prime_addOrderOf_dvd_card addOrderOf_nsmul_eq_zero IsUnit.exists_left_inv isUnit_iff_not_dvd_char Finite.of_fintype AddMonoid.addOrderOf_eq_one_iff ne_of_eq_of_ne Nat.Prime.ne_one Fact.out one_mul mul_assoc MulZeroClass.mul_zero nsmul_eq_mul

---

← Back to Index