theorem ERealFunction.argmin_eq_zeros_subdifferential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ↑(Set.Ioi ⊥)) : Argmin (Function.asEReal f) = (subdifferential f).zeros

Theorem 16.3: Fermat's rule. The global minimizers of an ]-∞,+∞]-valued function are exactly the zeros of its subdifferential.