mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s

Open mattrobball opened this issue 1 year ago • 2 comments
trafficstars

These are wrappers around the constructor and projection for Opposite Quiver.Hom _ _. The projection itself is reducible and with structure eta built in to defeq it seems like we might be making Lean work harder than is necessary.

Open in Gitpod

mattrobball avatar May 15 '24 16:05 mattrobball

!bench

mattrobball avatar May 15 '24 16:05 mattrobball

Here are the benchmark results for commit e909ecb0df49c3c96c769b4bf702a3d6084d240e.Found no runs to compare against.

leanprover-bot avatar May 16 '24 15:05 leanprover-bot