Commit 2024-10-23 15:47 9e3c1429

View on Github →

chore(Algebra/Category): restore lemmas lost from the port (#18112)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Basic.lean

added theorem CommRingCat.ofHom_apply'

added theorem CommRingCat.ofHom_apply

added theorem CommSemiRingCat.ofHom_apply'

added theorem CommSemiRingCat.ofHom_apply

added theorem RingCat.ofHom_apply'

added theorem RingCat.ofHom_apply

added theorem SemiRingCat.ofHom_apply'