Round trip, case by case: derivatives and quantities

Lean module Esm.Document.Math.Derivs, formal/Esm/Document/Math/Derivs.lean at 184aa13d35e5
Imports Esm.Document.Math.Templates

Generic steps

The time derivative

The spatial derivative

The spatial derivative with trailing operands

Quantities

This module also proves 21 lemmas without doc comments; they are in the source.