# Define a new Type in Lean: Tensor power of vector space

I want to define the tensor power of a vector space from the Lean library mathlib.

Here's the draft I have so far:

import data.complex.basic
import analysis.inner_product_space.basic
import linear_algebra.pi_tensor_product

open_locale tensor_product

notation ℋ^⊗n := ⨂[ℂ] i : fin n, ℋ

variables
(ℋ : Type) [inner_product_space ℂ ℋ]
(A : λ n : ℕ, ℋ^⊗n)


Any pointers are appreciated!

• I have an open PR that adds these, mathlib#14196
– Eric
May 24 at 10:37

As of about two hours after you asked this question, this exists in mathlib as tensor_power, with notation ⨂[ℂ]^n ℋ for the example you mention.
If you're also interested in tensor_algebras, there is another open PR of mine, mathlib#10255, which provides the result tensor_algebra R M ≃ₐ[R] (⨁ n, ⨂[R]^n M). I imagine this won't be merged for some time, as there are various technical issues to be resolved first.