Commit 2025-11-11 15:04 509f7084

View on Github →

feat(RingTheory/Perfection): lemmas for frobeniusEquiv.symm (#26386) This PR continues the work from #22330. Original PR: https://github.com/leanprover-community/mathlib4/pull/22330

Estimated changes

Modified Mathlib/FieldTheory/Perfect.lean

added theorem MonoidHom.map_frobeniusEquiv_symm

added theorem MonoidHom.map_iterate_frobeniusEquiv_symm

added theorem RingHom.map_frobeniusEquiv_symm

added theorem RingHom.map_iterate_frobeniusEquiv_symm

added theorem coe_frobeniusEquiv_symm_comp_coe_frobenius

added theorem coe_frobenius_comp_coe_frobeniusEquiv_symm

Modified Mathlib/RingTheory/Perfection.lean

deleted def ModP

added theorem Perfection.coeff_frobeniusEquiv_symm

added theorem Perfection.coeff_iterate_frobeniusEquiv_symm

added theorem PreTilt.coeff_frobenius

added theorem PreTilt.coeff_frobeniusEquiv_symm

added theorem PreTilt.coeff_frobenius_pow

added theorem PreTilt.coeff_iterate_frobeniusEquiv_symm

Modified Mathlib/RingTheory/Perfectoid/Untilt.lean

added theorem PreTilt.untilt_iterate_frobeniusEquiv_symm_pow