Theorems · Theorem · several complex variables

torusIntegral_radius_zero

∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E],
  n ≠ 0 → ∀ (f : (Fin n → ℂ) → E) (c : Fin n → ℂ), (∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0

Defined in

Mathlib.MeasureTheory.Integral.TorusIntegral

Cited by

0 results in Mathlib

Foundations

Depth 253 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace