tensors

Stream: maths

[Juho Kupiainen]

Does Lean code exist for working with tensors the classical way (https://en.wikipedia.org/wiki/Tensor#Tensor_product) with Einstein summation convention? I'm defining iterated linear maps and tensors using the definition of iterated_continuous_linear_map from mathlib/analysis/calculus/iterated..
I wonder if such definitions already exist. The Einstein summation convention is a bit tricky to implement.. Is there any way to give meaning to upper vs lower script arguments?

[Johan Commelin]

We don't have Einstein summation. We do have something called holors that I've never heard of before.

[Kevin Buzzard]

I don't know of any Lean code already there which will help. For upper and lower numbering with a fixed number of indices you could do it with notation I guess (maybe just with ^ and _ ?)

[Johan Commelin]

Of course ^ is already claimed by has_pow... but you could override that if you want.