Commit 2025-11-30 12:04 dc15895c

View on Github →

feat(RingTheory/AdjoinRoot): map (#32111) And golf algHomOfDvd, algHomOfAssociated using it. From Toric

Estimated changes

modified theorem AdjoinRoot.algHomOfDvd_root
modified theorem AdjoinRoot.coe_algEquivOfEq
modified theorem AdjoinRoot.coe_algHomOfDvd
added def AdjoinRoot.map
added theorem AdjoinRoot.map_of
added theorem AdjoinRoot.map_root
added theorem AdjoinRoot.ringHom_ext