Def ModuleCat.endMulEquiv

Modification history

2025-01-26 18:07

Mathlib/Algebra/Category/ModuleCat/Basic.lean

feat(Algebra): `Mul/RingEquiv`s between `center` and `Module.End` (#20721)

Deleted ModuleCat.endMulEquiv View on Github →

2024-12-05 09:31

Mathlib/Algebra/Category/ModuleCat/Basic.lean

refactor(Algebra/Category/ModuleCat): make `ModuleCat.Hom` a structure (#19511) …

Added ModuleCat.endMulEquiv View on Github →