Commit 2023-12-14 06:19 1d5e93af

View on Github →

feat(Algebra/CharP/ExpChar): add some results parallel to CharP (#8860)

change the condition of CharP.neg_one_pow_char and CharP.neg_one_pow_char_pow from CommRing to Ring
add ExpChar.exists, expChar_of_injective_algebraMap
add add_pow_expChar and 9 similar functions parallel to that of CharP
add {charP|charZero|expChar}_of_injective_ringHom

Estimated changes

Modified Mathlib/Algebra/CharP/Algebra.lean

added theorem charP_of_injective_ringHom

added theorem charZero_of_injective_ringHom

Modified Mathlib/Algebra/CharP/Basic.lean

modified theorem CharP.neg_one_pow_char

modified theorem CharP.neg_one_pow_char_pow

Modified Mathlib/Algebra/CharP/ExpChar.lean

added theorem ExpChar.exists

added theorem ExpChar.neg_one_pow_expChar

added theorem ExpChar.neg_one_pow_expChar_pow

added theorem add_pow_expChar

added theorem add_pow_expChar_of_commute

added theorem add_pow_expChar_pow

added theorem add_pow_expChar_pow_of_commute

added theorem expChar_of_injective_algebraMap

added theorem expChar_of_injective_ringHom

added theorem sub_pow_expChar

added theorem sub_pow_expChar_of_commute

added theorem sub_pow_expChar_pow

added theorem sub_pow_expChar_pow_of_commute