Commit 2024-08-10 12:31 ee220ded
View on Github →perf(Algebra.Ring.BooleanRing): scope simp theorems with weak keys but complex parameters (#15611)
The keys of these are the form HAdd.hAdd _ _ _ _ _ _ etc. but they require a typeclass search for BooleanRing which extends Ring. As they are only meant to apply to BooleanRings, we add a namespace and scope them to BooleanRing.