Commit 2024-10-24 20:59 a3c1388b

View on Github →

chore(Algebra/CharP): reduce theory requirements for CharP.Defs (#18182) The CharP/Defs.lean file imports some structures and proves quite a bit of theory. This PR tries to ensure that the focus is on the definitions instead, namely CharP, ringChar, ExpChar and ringExpChar. In the process, I made the following moves:

  • CharP/Basic.lean: renamed to CharP/Lemmas.lean
  • CharP/Defs.lean: all the lemmas that are not immediate consequences, or not needed to define ringChar or expChar have been moved to the new file CharP/Basic.lean Note that CharP/Basic.lean and CharP/Lemmas.lean can be imported independently. They are both unstructured collections of results so I'm not sure how we want to clean that up further.

Estimated changes

deleted theorem CharP.char_is_prime
deleted theorem MonoidHom.map_frobenius
deleted theorem RingHom.map_frobenius
deleted theorem add_pow_char
deleted theorem add_pow_char_of_commute
deleted theorem add_pow_char_pow
deleted theorem add_pow_expChar
deleted theorem add_pow_expChar_pow
deleted theorem add_pow_prime_eq
deleted theorem add_pow_prime_pow_eq
deleted theorem coe_iterateFrobenius
deleted theorem coe_iterateFrobenius_mul
deleted theorem exists_add_pow_prime_eq
deleted def frobenius
deleted theorem frobenius_def
deleted theorem frobenius_mul
deleted theorem frobenius_neg
deleted theorem frobenius_one
deleted theorem frobenius_sub
deleted def iterateFrobenius
deleted theorem iterateFrobenius_add
deleted theorem iterateFrobenius_def
deleted theorem iterateFrobenius_one
deleted theorem iterateFrobenius_zero
deleted theorem iterate_frobenius
deleted theorem list_sum_pow_char
deleted theorem list_sum_pow_char_pow
deleted theorem multiset_sum_pow_char
deleted theorem multiset_sum_pow_char_pow
deleted theorem neg_one_pow_char
deleted theorem neg_one_pow_char_pow
deleted theorem neg_one_pow_expChar
deleted theorem neg_one_pow_expChar_pow
deleted theorem sub_pow_char
deleted theorem sub_pow_char_of_commute
deleted theorem sub_pow_char_pow
deleted theorem sub_pow_expChar
deleted theorem sub_pow_expChar_pow
deleted theorem sum_pow_char
deleted theorem sum_pow_char_pow
deleted theorem CharP.intCast_injOn_Ico
deleted theorem CharP.natCast_injOn_Iio
deleted theorem RingHom.charP_iff_charP
added theorem CharP.char_is_prime
added theorem RingHom.map_frobenius
added theorem add_pow_char
added theorem add_pow_char_pow
added theorem add_pow_expChar
added theorem add_pow_expChar_pow
added theorem add_pow_prime_eq
added theorem add_pow_prime_pow_eq
added theorem coe_iterateFrobenius
added def frobenius
added theorem frobenius_def
added theorem frobenius_mul
added theorem frobenius_neg
added theorem frobenius_one
added theorem frobenius_sub
added def iterateFrobenius
added theorem iterateFrobenius_add
added theorem iterateFrobenius_def
added theorem iterateFrobenius_one
added theorem iterateFrobenius_zero
added theorem iterate_frobenius
added theorem list_sum_pow_char
added theorem list_sum_pow_char_pow
added theorem multiset_sum_pow_char
added theorem neg_one_pow_char
added theorem neg_one_pow_char_pow
added theorem neg_one_pow_expChar
added theorem sub_pow_char
added theorem sub_pow_char_pow
added theorem sub_pow_expChar
added theorem sub_pow_expChar_pow
added theorem sum_pow_char
added theorem sum_pow_char_pow