Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 05:20 e250eb41

View on Github →

feat(category/schur): a small corollary of the baby schur's lemma (#3239)

Estimated changes

Modified src/category_theory/schur.lean

added def category_theory.is_iso_equiv_nonzero

Modified src/category_theory/simple.lean

added theorem category_theory.id_nonzero