Theorem ModuleCat.inv_hom_apply

Modification history

2024-12-05 09:31

Mathlib/Algebra/Category/ModuleCat/Basic.lean

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

Added ModuleCat.inv_hom_apply View on Github →