Theorem powMulEquiv_eq_toMulEquiv_frobeniusEquiv

Modification history

2026-03-03 15:46
Mathlib/FieldTheory/Perfect.lean
feat(RingTheory): generalise perfection to monoids (#31007) …
Added powMulEquiv_eq_toMulEquiv_frobeniusEquivView on Github →