Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 23:52 e36656ee

View on Github →

chore(category_theory/monoidal): golf some proofs (#6894) Golfs proofs of tensor_left_iff, tensor_right_iff, left_unitor_tensor', right_unitor_tensor and unitors_equal - in particular removes the file monoidal/unitors as all it contained was a proof of unitors_equal which is a two line proof.

Estimated changes