Def LinearAlgebra.FreeProduct.asPowers

Modification history

2025-05-07 09:33

Mathlib/LinearAlgebra/FreeProduct/Basic.lean

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

Added LinearAlgebra.FreeProduct.asPowers View on Github →