∀ (G : Type u_6) (α : Type u_7) [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α),
  MeasureTheory.addCovolume G α ν = if funDom : MeasureTheory.HasAddFundamentalDomain G α ν then ν ⋯.choose else 0