Def CommRingCat.Hom.Simps.hom

Modification history

2025-01-27 14:13

Mathlib/Algebra/Category/Ring/Basic.lean

feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) …

Added CommRingCat.Hom.Simps.hom View on Github →