Zulip Chat Archive

Stream: maths

Topic: tensors


view this post on Zulip Juho Kupiainen (Dec 07 2019 at 14:13):

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?

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:15):

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

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 14:15):

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 _ ?)

view this post on Zulip Johan Commelin (Dec 07 2019 at 14:16):

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


Last updated: May 09 2021 at 11:09 UTC