Commit 2025-12-22 22:40 ca833177

View on Github →

chore(Algebra/Ring/Parity): generalize even_two and Even.mul_left/right (#33135)

  • Moved even_two from Semiring to AddMonoidWithOne.
  • Generalized Even.mul_left and Even.mul_right to only require Distrib related classes (LeftDistribClass and RightDistribClass) instead of a full Semiring.
  • Refactored the file structure with new sections to accommodate these minimal assumptions.

Estimated changes

modified theorem Even.mul_left
modified theorem Even.mul_right