Commit 2023-06-21 15:20 a7c74ebd

View on Github →

feat: port FieldTheory.Cardinality (#5345)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Cardinality.lean

added theorem Field.nonempty_iff

added theorem Fintype.isPrimePow_card_of_field

added theorem Fintype.nonempty_field_iff

added theorem Fintype.not_isField_of_card_not_prime_pow

added theorem Infinite.nonempty_field