Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 04:29 e52026f7

View on Github →

feat(integration): elementary version of FTC-1 (#15603) The goal is to have a nice statement for the undergrad list and for Mathematics in Lean.

Estimated changes