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.

Estimated changes

added theorem BooleanRing.add_self
added theorem BooleanRing.neg_eq
added theorem BooleanRing.sub_eq_add
deleted theorem add_eq_zero'
deleted theorem add_self
deleted theorem mul_add_mul
deleted theorem mul_one_add_self
deleted theorem mul_self
deleted theorem neg_eq
deleted theorem sub_eq_add