Theorem iterateFrobenius_eq_pow

Modification history

2025-04-02 09:50
Mathlib/Algebra/CharP/Frobenius.lean
refactor(Algebra/CharP): Frobenius map definition in `Mathlib.Algebra.CharP.Frobenius` (#23444) …
Modified iterateFrobenius_eq_powView on Github →
2025-03-14 03:11
Mathlib/Algebra/CharP/Lemmas.lean
feat: Galois groups of finite fields (#22885)
Added iterateFrobenius_eq_powView on Github →