Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 03:25 b7864434

View on Github →

chore(algebra/category/*): Added of_hom to all of the algebraic categories. (#9454) As suggested in the comments of #9416.

Estimated changes

added def Algebra.of_hom
added def CommRing.of_hom
added def Ring.of_hom
added def SemiRing.of_hom
added def CommGroup.of_hom
added def Group.of_hom
added def Module.of_hom
added def Mon.of_hom
added def Magma.of_hom
added def Semigroup.of_hom