Mathlib v3 is deprecated. Go to Mathlib v4

Def Mon.of_hom

Modification history

2021-10-01 03:25

src/algebra/category/Mon/basic.lean

chore(algebra/category/*): Added `of_hom` to all of the algebraic categories. (#9454) …

Added Mon.of_hom View on Github →