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, ℋ

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

Any pointers are appreciated!

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

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.