mathlib
e52026f7 - feat(integration): elementary version of FTC-1 (#15603)

Commit

3 years ago

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.

Author

PatrickMassot

Parents