5 kyu
Real Chebyshev
15 of 23monadius
Loading description...
Theorem Proving
Fundamentals
This comment has been reported as {{ abuseKindText }}.
Show
This comment has been hidden. You can view it now .
This comment can not be viewed.
- |
- Reply
- Edit
- View Solution
- Expand 1 Reply Expand {{ comments?.length }} replies
- Collapse
- Spoiler
- Remove
- Remove comment & replies
- Report
{{ fetchSolutionsError }}
-
-
Your rendered github-flavored markdown will appear here.
-
Label this discussion...
-
No Label
Keep the comment unlabeled if none of the below applies.
-
Issue
Use the issue label when reporting problems with the kata.
Be sure to explain the problem clearly and include the steps to reproduce. -
Suggestion
Use the suggestion label if you have feedback on how this kata can be improved.
-
Question
Use the question label if you have questions and/or need help solving the kata.
Don't forget to mention the language you're using, and mark as having spoiler if you include your solution.
-
No Label
- Cancel
Commenting is not allowed on this discussion
You cannot view this solution
There is no solution to show
Please sign in or sign up to leave a comment.
How can I tell which functions are allowed? My solution (which works on my own computer) uses only functions imported from
data.polynomial,data.complex.exponential, andanalysis.special_functions.trigonometric, but codewars gives me unknown identifier messages for some of these functions.Information about the supported Lean and Mathlib versions can be found here.
Thanks!
Lean v3.11.0 should be enabled, see https://github.com/codewars/codewars.com/wiki/List-of-Lean-Kata-to-Update
Lean 3.11.0 cannot be enabled because it is slow (importing some libraries is slow; this kumite demonstrates it). Hopefully, next versions of Lean will be fast enough for this kata.
Lean v3.11.0 should be enabled, see https://github.com/codewars/codewars.com/wiki/List-of-Lean-Kata-to-Update
This comment has been hidden.
Thank you for the suggestion. I added LEM to the list of allowed axioms.