Commit 2026-03-04 10:01 80f4a5fc

feat(RingTheory): Teichmuller map (#30989) Let R be an I-adically complete ring, and p be a prime number with p ∈ I. This PR constructs the Teichmüller map Perfection (R ⧸ I) p →*₀ R such that it composed with the quotient map R →+* R ⧸ I is the "0-th coefficient" map Perfection (R ⧸ I) p →+* R ⧸ I. This generalises the existing PreTilt.untilt. I have also moved Mathlib/LinearAlgebra/SModEq to a folder to be /SModEq/Basic.lean, because I needed to add some lemmas to /SModEq/Prime.lean; I also added a lemma to the end of /Basic.lean called ideal.