Theorem Perfection.pthRootMonoidHom_eq_powMulEquiv_symm

Modification history

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