Theorems · Definition · measure theory
parallelepiped
{ι : Type u_1} → {E : Type u_3} → [Fintype ι] → [inst : AddCommGroup E] → [Module ℝ E] → (ι → E) → Set EThe closed parallelepiped spanned by a finite family of vectors.
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Fintypestatement and proof · cited by 7,736
- Set.imageproof · cited by 5,609
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- Set.Iccproof · cited by 1,702
Cited by26
Results whose statement or proof uses this declaration.
- Module.Basis.parallelepipedproof · cited by 12
- Module.Basis.map_addHaarproof · cited by 5
- OrthonormalBasis.volume_parallelepipedstatement and proof · cited by 4
- Module.Basis.addHaar_selfstatement and proof · cited by 3
- Module.Basis.parallelepiped_basisFunproof · cited by 3
- parallelepiped_basis_eqstatement · cited by 3
- parallelepiped_comp_equivstatement · cited by 3
- image_parallelepipedstatement · cited by 3
- Orientation.measure_orthonormalBasisstatement and proof · cited by 2
- Module.Basis.coe_parallelepipedstatement · cited by 2
- parallelepiped_eq_sum_segmentstatement · cited by 2
- ZSpan.fundamentalDomain_ae_parallelepipedstatement and proof · cited by 2