Commit 2025-03-15 13:13 4104be55

View on Github →

feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map.

Estimated changes

Modified Mathlib/Algebra/Field/Subfield/Basic.lean

added theorem RingHom.rangeRestrictField_bijective

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.Splits.mem_subfield_of_isRoot

Modified Mathlib/FieldTheory/Finite/Basic.lean

added theorem Subfield.card_bot

added def Subfield.fintypeBot

added theorem Subfield.mem_bot_iff_pow_eq_self

added theorem Subfield.roots_X_pow_char_sub_X_bot

added theorem Subfield.splits_bot

modified theorem ZMod.expand_card

added theorem ZMod.fieldRange_castHom_eq_bot

modified theorem ZMod.orderOf_dvd_card_sub_one

modified theorem ZMod.orderOf_units_dvd_card_sub_one

modified theorem ZMod.pow_card

modified theorem ZMod.pow_card_pow

modified theorem ZMod.pow_card_sub_one

modified theorem ZMod.pow_card_sub_one_eq_one

added theorem mem_bot_iff_intCast