Theorems · Theorem · measure theory

parallelepiped_eq_sum_segment

∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E),
  parallelepiped v = ∑ i, segment ℝ 0 (v i)

Defined in

Mathlib.MeasureTheory.Measure.Haar.OfBasis

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeAddCommGroupModule