Commit 2025-12-15 09:35 7fbf73cd

View on Github →

refactor: turn RootSystem into a mixin rather than extending RootPairing (#32885) The motivating benefits are:

  • Saving us from having to duplicate instances
  • Solving namespace issues such where to put lemmas about RootPairing.Base which are true only for RootSystems
  • Allowing us to drop a few .toRootPairing I see no downsides.

Estimated changes

added def RootPairing.mk''
deleted def RootSystem.mk'
deleted structure RootSystem