Def ModuleCat.restrictScalarsEquivalenceOfRingEquiv

Modification history

2026-04-19 10:51

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

chore(Algebra/Category): add `ModuleCat.restrictScalarsIsoOfEquiv` (#37773) …

Modified ModuleCat.restrictScalarsEquivalenceOfRingEquiv View on Github →

2024-05-08 11:06

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

refactor(CategoryTheory): make Functor.IsEquivalence a Prop (#12462) …

Added ModuleCat.restrictScalarsEquivalenceOfRingEquiv View on Github →