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.