使用精益使E-222正式化 此回购协议是尝试在E-222讲座中进行的工作,同时生成注释的TeX版本并在Lean中使工作正式化。 对于任何讲座或习题集,目标是使注释和假设尽可能与材料的流程接近。 例如,在讨论可逆矩阵时,我们没有证明det(AB) = det(A)det(B) ,因为讲座没有。 但是,为了展示精益,我们可以自行定义双射是什么,而不是使用内部定义。 随着讲座的累积,将建立正式的小组。 如果精益和mathlib所依赖的不同,则可以突出显示这些差异,然后加以解决或进行对比。