tensor calculus

Stream: Is there code for X?

[Anthony Bordg]

Is tensor calculus formalized in mathlib (or in any other proof assistant)?

[Patrick Massot]

Not in mathlib, and not in any other proof assistant as far as I know.

[Patrick Massot]

mathlib isn't far, and Isabelle should be pretty close too.

[Anthony Bordg]

@Patrick Massot Thanks for your answer.

[Joseph Tooby-Smith]

In case people stumble across this post: I have aspects of Tensor calculus for Lorentz tensors here. This follows a modular-operad approach. Just the beginning now, but I am developing it further.