论文标题
为卷积设计通用图书馆
Designing a general library for convolutions
论文作者
论文摘要
我们将讨论通过建立正式图书馆来卷积两个功能的经验和设计决策。卷积是一个基本概念，在整个数学中都有应用。我们将重点关注使卷积一般且易于使用的设计决策，并将这种开发纳入Lean的数学库Mathlib。
We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib.
