lean-inf
Compute with infinities and infinitesimals! A calculator using the Levi-Civita field, implemented in Lean 4 as a datatype. Gives autodiff for free.
lean-inf
Levi-Civita field implementation in Lean 4 for computing with infinities and infinitesimals.