Mathlib v3 is deprecated. Go to Mathlib v4

Def Magma.of_hom

Modification history

2022-04-20 18:42
src/algebra/category/Semigroup/basic.lean
feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526) …
Modified Magma.of_homView on Github →
2021-10-01 03:25
src/algebra/category/Semigroup/basic.lean
chore(algebra/category/*): Added `of_hom` to all of the algebraic categories. (#9454) …
Added Magma.of_homView on Github →