Commit 2024-11-17 19:21 38affacc

chore: use AlgHom.restrictDomain (#19116) I previously didn't know the existence of AlgHom.restrictDomain and wrote many lemmas using a longer expression that is exactly the definition of AlgHom.restrictDomain; I'm now changing all these lemmas to use AlgHom.restrictDomain. There are more appearances of .comp (IsScalarTower.toAlgHom but either the file doesn't import AlgHom.restrictDomain, or using it breaks the proof, so I only replaced one appearance.