Commit 2026-03-05 10:25 4646bc64

View on Github →

chore: reduce defeq abuse (#35286) Cherry-picked from #35182, improved

Estimated changes

Modified Mathlib/Algebra/Module/SnakeLemma.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

modified theorem AddMonoidAlgebra.single_mem_grade

Modified Mathlib/RingTheory/AdjoinRoot.lean

added def AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk

added theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk

added theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk

deleted def AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk

deleted theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk

deleted theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk

added def AdjoinRoot.quotMapOfEquivQuotMapCMapMk

added theorem AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk

added theorem AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk

deleted def AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk

deleted theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk

deleted theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk

Modified Mathlib/RingTheory/Kaehler/Basic.lean

added theorem KaehlerDifferential.fromIdeal_surjective

Modified Mathlib/RingTheory/KrullDimension/Polynomial.lean