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

Question

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!

Answer 1

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.