Theorem PreTilt.exists_smodEq_untiltAux

Modification history

2026-03-04 10:01
Mathlib/RingTheory/Perfectoid/Untilt.lean
feat(RingTheory): Teichmuller map (#30989) …
Deleted PreTilt.exists_smodEq_untiltAuxView on Github →
2025-02-20 10:22
Mathlib/RingTheory/Perfectoid/Untilt.lean
feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) …
Added PreTilt.exists_smodEq_untiltAuxView on Github →