Commit 2025-12-01 21:50 5fc7bcb5

View on Github →

refactor(RingTheory/Perfection): add PreTilt.coeff (#32248) In this PR, we separate PreTilt.coeff from Perfection.coeff to solve the abuse defeq problem between PreTilt O p and Perfection (ModP O p) p.

Estimated changes

Modified Mathlib/RingTheory/Perfection.lean

added def PreTilt.coeff

added theorem PreTilt.coeff_def

deleted theorem PreTilt.coeff_frobenius_pow

added theorem PreTilt.coeff_iterate_frobenius'

added theorem PreTilt.coeff_iterate_frobenius

modified theorem PreTilt.coeff_nat_find_add_ne_zero

added theorem PreTilt.coeff_pow_p

modified theorem PreTilt.valAux_eq

Modified Mathlib/RingTheory/Perfectoid/FontaineTheta.lean

Modified Mathlib/RingTheory/Perfectoid/Untilt.lean