文件列表:

.vscode/
BET/
BET.lean
CONTRIBUTING.md
LICENSE
lake-manifest.json
lakefile.lean
lean-toolchain

# Birkhoff's ergodic theorem in Lean 4  This project was initiated at the [Machine-Checked Mathematics Workshop](https://www.lorentzcenter.nl/machine-checked-mathematics.html) at the Lorentz Center, 10-14 July 2023. Developed with @mseri, @marcolenci and Guillaume Dubach, under the support and supervision of Sébastien Gouzel. ## How to use Make sure that Lean 4 is installed, if not, [start here](https://leanprover-community.github.io/). Clone this repo ``` git clone https://github.com/mseri/birkhoff.git ``` then enter the folder ``` cd birkhoff ``` download mathlib's cache ``` lake exe cache get ``` and open the folder in vscode to view and edit the Lean code. [Contribution guidelines](CONTRIBUTING.md) for this project.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：