Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(analysis/analytic/basic.lean): fix latex in doc (#5397)
Doc in the file `analytic/basic.lean` is broken, since I used a latex command `\choose` which doesn't exist. Replace it with `\binom`.
- Loading branch information