Interest: a Lean library for financial mathematics