Primitives_which_Differ_by_Constant
Provedantiderivativescalculusproofwiki
If F and G have the same derivative on an interval, they differ by a constant.
Preamble
import Mathlib.Analysis.Calculus.Deriv.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.Deriv.Basic theorem Primitives_which_Differ_by_Constant (F G : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hF : DifferentiableOn ℝ F (Set.Ioo a b)) (hG : DifferentiableOn ℝ G (Set.Ioo a b)) (h : ∀ x ∈ Set.Ioo a b, deriv F x = deriv G x) : ∃ c : ℝ, ∀ x ∈ Set.Ioo a b, F x = G x + c := by sorry
Source