Commit 2024-02-14 03:21 3809ca5a

View on Github →

feat(FieldTheory/Perfect): add various convenient lemmas for iterateFrobenius[Equiv] (#10405)

Estimated changes

Modified Mathlib/Algebra/CharP/ExpChar.lean

modified theorem coe_iterateFrobenius_mul

added theorem iterateFrobenius_add_apply

added theorem iterateFrobenius_mul_apply

modified theorem iterateFrobenius_one

added theorem iterateFrobenius_one_apply

modified theorem iterateFrobenius_zero

added theorem iterateFrobenius_zero_apply

Modified Mathlib/FieldTheory/Perfect.lean

added theorem frobeniusEquiv_def

added theorem iterateFrobeniusEquiv_add

added theorem iterateFrobeniusEquiv_add_apply

added theorem iterateFrobeniusEquiv_def

added theorem iterateFrobeniusEquiv_one

added theorem iterateFrobeniusEquiv_one_apply

added theorem iterateFrobeniusEquiv_symm_add

added theorem iterateFrobeniusEquiv_symm_add_apply

added theorem iterateFrobeniusEquiv_zero

added theorem iterateFrobeniusEquiv_zero_apply