Commit 2025-05-07 09:33 8ac52a50

View on Github →

refactor: rename LinearAlgebra.FreeProductOfPowers to LinearAlgebra.FreeProduct.asPowers, add simp shortcut to lift lemmas (#24531)

  • Change names of FreeProductOfPowers to FreeProduct.asPowers and equivPowerAlgebra to equivAsPowers, in preparation for a feat adding API for the power algebra formulation.
  • Add convenience "simp shortcut" attributes to some lift lemmas.

Estimated changes