Zulip Chat Archive

Stream: Is there code for X?

Topic: Fermat's lemma

Jiatong Yang (Nov 11 2024 at 05:15):

Is there code for Fermat's lemma, which states that the derivative at a local minimum(maximum) is zero?

Daniel Weber (Nov 11 2024 at 05:51):

Yes, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/LocalExtr/Basic.html#Fermat-s-Theorem

Last updated: May 02 2025 at 03:31 UTC