Theorem iterateFrobeniusEquiv_one_apply

Modification history

2024-02-14 03:21

Mathlib/FieldTheory/Perfect.lean

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

Added iterateFrobeniusEquiv_one_apply View on Github →