Fintype.nonempty_field_iff
theorem Fintype.nonempty_field_iff :
∀ {α : Type u_1} [inst : Fintype α], Nonempty (Field α) ↔ IsPrimePow (Fintype.card α)
The theorem states that a finite type, denoted as `α`, can be given a field structure if and only if the number of elements in `α` (or its cardinality denoted by `Fintype.card α`) is a power of a prime number. In other words, there exists a field structure on a finite type if and only if there is a prime number `p` and a positive natural number `k` such that the number of elements in the finite type can be expressed as `p^k`.
More concisely: A finite type `α` has a field structure if and only if the cardinality of `α` is a power of a prime number.
|
Field.nonempty_iff
theorem Field.nonempty_iff : ∀ {α : Type u}, Nonempty (Field α) ↔ IsPrimePow (Cardinal.mk α)
The theorem `Field.nonempty_iff` states that a type `α` can have a field structure if and only if its cardinality, the number of elements it contains, can be expressed as a power of a prime number. This is to say, there exists a prime number `p` and a positive integer `k` such that `p^k` equals the cardinality of the type `α`.
More concisely: A type `α` has a field structure if and only if its cardinality can be expressed as a power of a prime number.
|
Infinite.nonempty_field
theorem Infinite.nonempty_field : ∀ {α : Type u} [inst : Infinite α], Nonempty (Field α)
This theorem states that if there exists a type `α` which is infinite (meaning it has infinitely many distinct elements), then it is possible to endow this type with a field structure. A field in mathematics is a set with two operations (usually referred to as addition and multiplication) that are commutative, associative, have identities, and every non-zero element has an additive and a multiplicative inverse.
More concisely: If a type `α` is infinite, then it can be equipped with a field structure.
|
Fintype.isPrimePow_card_of_field
theorem Fintype.isPrimePow_card_of_field :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Field α], IsPrimePow (Fintype.card α)
This theorem states that for any finite field, the number of elements in the field, also known as the field's cardinality, is a prime power. In other words, the cardinality of the field can be written as a prime number raised to a positive natural number.
More concisely: Every finite field has a cardinality that is a power of a prime number.
|