Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-21 15:59 897e4ed6

View on Github →

feat(field_theory): finite fields exist (#8692)

Estimated changes

Modified src/algebra/char_p/algebra.lean

added theorem algebra.char_p_iff

Modified src/algebra/char_p/basic.lean

added theorem char_p.neg_one_pow_char

added theorem char_p.neg_one_pow_char_pow

modified theorem ring_hom.char_p_iff_char_p

Modified src/algebra/group_power/lemmas.lean

added theorem commute.cast_int_left

added theorem commute.cast_int_right

Modified src/data/fintype/basic.lean

added theorem fintype.one_lt_card

Modified src/data/polynomial/algebra_map.lean

added theorem polynomial.coeff_zero_eq_aeval_zero'

Created src/data/zmod/algebra.lean

added def zmod.algebra'

Modified src/data/zmod/basic.lean

Modified src/field_theory/finite/basic.lean

added theorem card_eq_pow_finrank

added theorem finite_field.X_pow_card_pow_sub_X_nat_degree_eq

added theorem finite_field.X_pow_card_pow_sub_X_ne_zero

added theorem finite_field.X_pow_card_sub_X_nat_degree_eq

added theorem finite_field.X_pow_card_sub_X_ne_zero

added theorem finite_field.pow_card_pow

added theorem finite_field.roots_X_pow_card_sub_X

added theorem zmod.pow_card_pow

Created src/field_theory/finite/galois_field.lean

added theorem galois_field.card

added def galois_field.equiv_zmod_p

added theorem galois_field.finrank

added theorem galois_field.splits_zmod_X_pow_sub_X

added def galois_field

added theorem galois_poly_separable

Modified src/field_theory/separable.lean

added theorem polynomial.exists_finset_of_splits

added theorem polynomial.not_separable_zero

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_univ