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?
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.
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 _ ?)
Johan Commelin (Dec 07 2019 at 14:16):
^ is already claimed by
has_pow... but you could override that if you want.
Last updated: May 09 2021 at 11:09 UTC