Commit 2023-06-02 12:18 7412bcf6

View on Github →

feat: port FieldTheory.Finite.Basic (#4583)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Finite/Basic.lean

added theorem CharP.sq_add_sq

added theorem FiniteField.X_pow_card_pow_sub_X_natDegree_eq

added theorem FiniteField.X_pow_card_pow_sub_X_ne_zero

added theorem FiniteField.X_pow_card_sub_X_natDegree_eq

added theorem FiniteField.X_pow_card_sub_X_ne_zero

added theorem FiniteField.card'

added theorem FiniteField.card

added theorem FiniteField.card_image_polynomial_eval

added theorem FiniteField.cast_card_eq_zero

added theorem FiniteField.even_card_iff_char_two

added theorem FiniteField.even_card_of_char_two

added theorem FiniteField.exists_nonsquare

added theorem FiniteField.exists_root_sum_quadratic

added theorem FiniteField.expand_card

added theorem FiniteField.forall_pow_eq_one_iff

added theorem FiniteField.frobenius_pow

added theorem FiniteField.isSquare_iff

added theorem FiniteField.isSquare_of_char_two

added theorem FiniteField.odd_card_of_char_ne_two

added theorem FiniteField.pow_card

added theorem FiniteField.pow_card_pow

added theorem FiniteField.pow_card_sub_one_eq_one

added theorem FiniteField.pow_dichotomy

added theorem FiniteField.prod_univ_units_id_eq_neg_one

added theorem FiniteField.roots_X_pow_card_sub_X

added theorem FiniteField.sum_pow_lt_card_sub_one

added theorem FiniteField.sum_pow_units

added theorem FiniteField.unit_isSquare_iff

added theorem Int.ModEq.pow_card_sub_one_eq_one

added theorem Nat.ModEq.pow_totient

added theorem ZMod.card_units

added theorem ZMod.expand_card

added theorem ZMod.frobenius_zMod

added theorem ZMod.orderOf_dvd_card_sub_one

added theorem ZMod.orderOf_units_dvd_card_sub_one

added theorem ZMod.pow_card

added theorem ZMod.pow_card_pow

added theorem ZMod.pow_card_sub_one_eq_one

added theorem ZMod.pow_totient

added theorem ZMod.sq_add_sq

added theorem ZMod.units_pow_card_sub_one_eq_one

added theorem card_eq_pow_finrank