`BookProof.WeylCauchyRiemann.integral_fderiv_one_eq_zero` {ψ : ℂ → ℂ} (hψ : ContDiff ℝ ∞ ψ) (hψc : HasCompactSupport ψ) : ∫ z : ℂ, fderiv ℝ ψ z 1 = 0

Initializing...

`BookProof.WeylCauchyRiemann.integral_fderiv_one_eq_zero` {ψ : ℂ → ℂ} (hψ : ContDiff ℝ ∞ ψ) (hψc : HasCompactSupport ψ) : ∫ z : ℂ, fderiv ℝ ψ z 1 = 0 · Prove2Me