Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 20:58 e8339bd6

View on Github →

feat(category_theory/fully_faithful): nat_trans_of_comp_fully_faithful (#13327) I added nat_iso_of_comp_fully_faithful in an earlier PR, but left out the more basic construction.

Estimated changes