periodic_deriv

lemma periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]    {f : 𝕜 → F} {T : 𝕜} (diff_f : ContDiff 𝕜 1 f) (periodic_f : f.Periodic T) : (deriv f).Periodic T := by  intro x  set g : 𝕜 → 𝕜 := fun x ↦ x + T with gdef  have diff_g : Differentiable 𝕜 g := differentiable_id.add_const _  have : deriv (f ∘ g) x = ((deriv f) ∘ g) x := by    calc deriv (f ∘ g) x      _ = deriv g x • deriv f (g x) := deriv.scomp x (diff_f.differentiable (by norm_num)).differentiableAt diff_g.differentiableAt      _ = deriv f (g x) := by rw [gdef, deriv_add_const, deriv_id'']; simp  rw [gdef] at this  simp only [Function.comp_apply] at this  convert this.symm  ext y  simp [(periodic_f y).symm]