Commit 2026-10-08 14:19 59cf8085

View on Github →

feat(Algebra/CharP/Two): weaken theorem hypothesis (#42346) This PR weakens the hypothesis of several theorems about rings of characteristic 2. Some of these lemmas do not require the (semi)ring to be associative, some of them do not require subtraction (and thus Ring can be weakened to Semiring), and those about integer cast do not even require multiplication.

Estimated changes

modified theorem CharTwo.list_sum_mul_self
modified theorem CharTwo.list_sum_sq
modified theorem CharTwo.multiset_sum_sq
added theorem CharTwo.neg_natCast_eq
added theorem CharTwo.neg_one_eq_one
modified theorem CharTwo.sum_sq