Theorem AlgEquiv.toRingEquiv_restrictScalars

Modification history

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