Theorem Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk

Modification history

2026-03-05 10:25
Mathlib/RingTheory/Teichmuller.lean
feat(RingTheory): isomorphism between perfection of R and perfection of R/I (#36161) …
Added Perfection.teichmuller₀_mapMonoidHom_idealQuotientMkView on Github →