Theorem AlgEquiv.restrictScalarsHom_injective

Modification history

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