Theorems · Theorem · measure theory
Complex.volume_preserving_equiv_pi
MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivPi) MeasureTheory.volume MeasureTheory.volume
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites35
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- MeasurableSpaceproof · cited by 13,106
- MeasureTheory.Measureproof · cited by 10,939
- Complexstatement and proof · cited by 5,565
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- MeasureTheory.Measure.mapproof · cited by 858
- DFunLikeproof · cited by 576
- ContinuousLinearEquiv.symmproof · cited by 368
- MeasurableEquivstatement and proof · cited by 269
- MeasureTheory.MeasurePreservingstatement and proof · cited by 259
- MeasurableEquiv.symmproof · cited by 155
Cited by2
Results whose statement or proof uses this declaration.
- Complex.volume_preserving_equiv_real_prodproof · cited by 7
- NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasisproof · cited by 2