Def LinearAlgebra.FreeProduct.asPowers

Modification history

2026-06-23 00:12

Mathlib/LinearAlgebra/FreeProduct/Basic.lean

refactor: switch from RingQuot to RingCon.Quotient (#40451) …

Modified LinearAlgebra.FreeProduct.asPowers View on Github →

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 →