Def LinearAlgebra.FreeProduct_ofPowers

Modification history

2024-12-08 15:02

Mathlib/LinearAlgebra/FreeProduct/Basic.lean

chore(*): rename some `defs` to `camelCase` (#19795)

Deleted LinearAlgebra.FreeProduct_ofPowers View on Github →

2024-07-19 14:02

Mathlib/LinearAlgebra/FreeProduct/Basic.lean

feat (LinearAlgebra/FreeProduct): introduce basic structure, universal property (#14858) …

Added LinearAlgebra.FreeProduct_ofPowers View on Github →