Theorem AlgEquiv.restrictScalarsHom_apply

Modification history

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