Theorem AlgEquiv.toMonoidHom_symm_extendScalarsHomOfSurjective

Modification history

2026-07-10 02:42
Mathlib/Algebra/Algebra/Tower.lean
feat(Algebra/Algebra/Tower): add `restrictScalarsHom` (#41417) …
Added AlgEquiv.toMonoidHom_symm_extendScalarsHomOfSurjectiveView on Github →