Cardinality

📁 Source: Mathlib/FieldTheory/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems nonempty_iff, isPrimePow_card_of_field, nonempty_field_iff, not_isField_of_card_not_prime_pow, nonempty_field	5
Total	5

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_iff 📖	mathematical	—	Field IsPrimePow Cardinal Cardinal.instCommMonoidWithZero	—	Cardinal.isPrimePow_iff Cardinal.mk_fintype LT.lt.not_ge Cardinal.natCast_lt_aleph0 Cardinal.instCharZero Fintype.nonempty_field_iff Infinite.nonempty_field

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrimePow_card_of_field 📖	mathematical	—	IsPrimePow Nat.instCommMonoidWithZero card	—	FiniteField.isPrimePow_card
nonempty_field_iff 📖	mathematical	—	Field IsPrimePow Nat.instCommMonoidWithZero card	—	isPrimePow_card_of_field Prime.nat_prime card_eq_nat_card GaloisField.card LT.lt.ne'
not_isField_of_card_not_prime_pow 📖	mathematical	IsPrimePow Nat.instCommMonoidWithZero card	IsField Ring.toSemiring	—	nonempty_field_iff

Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_field 📖	mathematical	—	Field	—	Cardinal.mk_fractionRing MvPolynomial.cardinalMk_eq_max_lift Nontrivial.to_nonempty instNontrivial ULift.nontrivial Rat.nontrivial Cardinal.mk_eq_aleph0 instCountableULift Encodable.countable instInfiniteULift NoMinOrder.infinite instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing Cardinal.lift_id sup_of_le_right sup_of_le_left Nonempty.map MvPolynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain Cardinal.eq

---

← Back to Index