PolarCoord

📁 Source: Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

Statistics

Metric	Count
Definitions FDerivPolarCoordRealSymm, homeoRealMixedSpacePolarSpace, measurableEquivRealMixedSpacePolarSpace, mixedSpaceToRealMixedSpace, polarCoord, polarCoordReal, polarSpace, polarSpaceCoord, realMixedSpace	9
Theorems det_fderivPolarCoordRealSymm, hasFDerivAt_polarCoordReal_symm, homeoRealMixedSpacePolarSpace_apply, homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, homeoRealMixedSpacePolarSpace_apply_snd, homeoRealMixedSpacePolarSpace_symm_apply, instIsAddHaarMeasureRealMixedSpaceVolume, integral_comp_polarCoordReal_symm, integral_comp_polarCoord_symm, integral_comp_polarSpaceCoord_symm, lintegral_comp_polarCoordReal_symm, lintegral_comp_polarCoord_symm, lintegral_comp_polarSpaceCoord_symm, measurable_polarCoordReal_symm, measurable_polarCoord_symm, measurable_polarSpaceCoord_symm, mixedSpaceToRealMixedSpace_apply, normAtComplexPlaces_polarSpaceCoord_symm, normAtPlace_polarCoord_symm_of_isComplex, normAtPlace_polarCoord_symm_of_isReal, polarCoordReal_apply, polarCoordReal_source, polarCoordReal_symm_target_ae_eq_univ, polarCoordReal_target, polarCoord_apply, polarCoord_source, polarCoord_symm_apply, polarCoord_symm_eq, polarCoord_target, polarCoord_target_eq_polarCoordReal_target, polarSpaceCoord_apply, polarSpaceCoord_source, polarSpaceCoord_symm_apply, polarSpaceCoord_target, polarSpaceCoord_target', volume_eq_two_pi_pow_mul_integral, volume_eq_two_pow_mul_two_pi_pow_mul_integral, volume_preserving_homeoRealMixedSpacePolarSpace, volume_preserving_mixedSpaceToRealMixedSpace_symm	40
Total	49

NumberField.mixedEmbedding

Definitions

Name	Category	Theorems
FDerivPolarCoordRealSymm 📖	CompOp	2 math math: hasFDerivAt_polarCoordReal_symm, det_fderivPolarCoordRealSymm
homeoRealMixedSpacePolarSpace 📖	CompOp	8 math math: polarSpaceCoord_target, homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, volume_preserving_homeoRealMixedSpacePolarSpace, homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply, polarSpaceCoord_apply, homeoRealMixedSpacePolarSpace_apply_snd, homeoRealMixedSpacePolarSpace_symm_apply
measurableEquivRealMixedSpacePolarSpace 📖	CompOp	—
mixedSpaceToRealMixedSpace 📖	CompOp	3 math math: volume_preserving_mixedSpaceToRealMixedSpace_symm, mixedSpaceToRealMixedSpace_apply, polarCoord_symm_eq
polarCoord 📖	CompOp	11 math math: lintegral_comp_polarCoord_symm, normAtPlace_polarCoord_symm_of_isComplex, polarCoord_symm_apply, polarCoord_source, polarCoord_target, normAtPlace_polarCoord_symm_of_isReal, polarCoord_symm_eq, measurable_polarCoord_symm, polarCoord_apply, polarCoord_target_eq_polarCoordReal_target, integral_comp_polarCoord_symm
polarCoordReal 📖	CompOp	10 math math: measurable_polarCoordReal_symm, polarCoordReal_apply, polarCoordReal_source, polarCoord_symm_eq, lintegral_comp_polarCoordReal_symm, hasFDerivAt_polarCoordReal_symm, polarCoordReal_symm_target_ae_eq_univ, polarCoord_target_eq_polarCoordReal_target, polarCoordReal_target, integral_comp_polarCoordReal_symm
polarSpace 📖	CompOp	15 math math: integral_comp_polarSpaceCoord_symm, polarSpaceCoord_target, normAtComplexPlaces_polarSpaceCoord_symm, polarSpaceCoord_symm_apply, polarSpaceCoord_target', homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, volume_preserving_homeoRealMixedSpacePolarSpace, homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply, polarSpaceCoord_apply, homeoRealMixedSpacePolarSpace_apply_snd, polarSpaceCoord_source, homeoRealMixedSpacePolarSpace_symm_apply, measurable_polarSpaceCoord_symm, lintegral_comp_polarSpaceCoord_symm
polarSpaceCoord 📖	CompOp	9 math math: integral_comp_polarSpaceCoord_symm, polarSpaceCoord_target, normAtComplexPlaces_polarSpaceCoord_symm, polarSpaceCoord_symm_apply, polarSpaceCoord_target', polarSpaceCoord_apply, polarSpaceCoord_source, measurable_polarSpaceCoord_symm, lintegral_comp_polarSpaceCoord_symm
realMixedSpace 📖	CompOp	31 math math: lintegral_comp_polarCoord_symm, measurable_polarCoordReal_symm, normAtPlace_polarCoord_symm_of_isComplex, polarCoordReal_apply, polarSpaceCoord_target, polarCoordReal_source, polarCoord_symm_apply, volume_preserving_mixedSpaceToRealMixedSpace_symm, polarCoord_source, mixedSpaceToRealMixedSpace_apply, polarCoord_target, normAtPlace_polarCoord_symm_of_isReal, polarCoord_symm_eq, homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, volume_preserving_homeoRealMixedSpacePolarSpace, homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, lintegral_comp_polarCoordReal_symm, measurable_polarCoord_symm, polarCoord_apply, hasFDerivAt_polarCoordReal_symm, homeoRealMixedSpacePolarSpace_apply, polarCoordReal_symm_target_ae_eq_univ, polarSpaceCoord_apply, homeoRealMixedSpacePolarSpace_apply_snd, polarCoord_target_eq_polarCoordReal_target, instIsAddHaarMeasureRealMixedSpaceVolume, homeoRealMixedSpacePolarSpace_symm_apply, det_fderivPolarCoordRealSymm, polarCoordReal_target, integral_comp_polarCoord_symm, integral_comp_polarCoordReal_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_fderivPolarCoordRealSymm 📖	mathematical	—	ContinuousLinearMap.det Real Real.commRing realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Prod.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Prod.instModule Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Prod.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal FDerivPolarCoordRealSymm Finset.prod Real.instCommMonoid Finset.univ Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype	—	ContinuousLinearMap.det.eq_1 LinearMap.det_prodMap Module.Free.function Subtype.finite Finite.of_fintype Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Real.instIsDomain FiniteDimensional.rclike_to_real instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.Free.prod FiniteDimensional.finiteDimensional_pi' Module.Finite.prod LinearMap.det_id one_mul det_fderivPiPolarCoordSymm
hasFDerivAt_polarCoordReal_symm 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField realMixedSpace Prod.instAddCommGroup Pi.addCommGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.instAddCommGroup NumberField.InfinitePlace.IsComplex Prod.instModule Real.semiring Pi.addCommMonoid Real.instAddCommMonoid Prod.instAddCommMonoid Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm polarCoordReal FDerivPolarCoordRealSymm	—	HasFDerivAt.prodMap hasFDerivAt_id hasFDerivAt_pi_polarCoord_symm Subtype.finite Finite.of_fintype
homeoRealMixedSpacePolarSpace_apply 📖	mathematical	—	DFunLike.coe Homeomorph realMixedSpace polarSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex EquivLike.toFunLike Homeomorph.instEquivLike homeoRealMixedSpacePolarSpace NumberField.InfinitePlace.not_isReal_iff_isComplex	—	—
homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex 📖	mathematical	—	DFunLike.coe Homeomorph realMixedSpace polarSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex EquivLike.toFunLike Homeomorph.instEquivLike homeoRealMixedSpacePolarSpace	—	NumberField.InfinitePlace.not_isReal_iff_isComplex Subtype.prop
homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal 📖	mathematical	—	DFunLike.coe Homeomorph realMixedSpace polarSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex EquivLike.toFunLike Homeomorph.instEquivLike homeoRealMixedSpacePolarSpace	—	NumberField.InfinitePlace.not_isReal_iff_isComplex Subtype.prop
homeoRealMixedSpacePolarSpace_apply_snd 📖	mathematical	—	DFunLike.coe Homeomorph realMixedSpace polarSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex EquivLike.toFunLike Homeomorph.instEquivLike homeoRealMixedSpacePolarSpace	—	—
homeoRealMixedSpacePolarSpace_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph polarSpace realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex NumberField.InfinitePlace.IsReal EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeoRealMixedSpacePolarSpace	—	—
instIsAddHaarMeasureRealMixedSpaceVolume 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure realMixedSpace Prod.instAddGroup Pi.addGroup NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instAddGroup NumberField.InfinitePlace.IsComplex instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.prod.instIsAddHaarMeasure MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd Real.borelSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Prod.borelSpace secondCountableTopologyEither_of_right Prod.continuousAdd MeasureTheory.Measure.instSigmaFiniteProdVolume instIsAddHaarMeasureProdRealVolume MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume Pi.measurableAdd
integral_comp_polarCoordReal_symm 📖	mathematical	—	MeasureTheory.integral realMixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoordReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Finset.prod Real.instCommMonoid Finset.univ OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	MeasureTheory.setIntegral_univ MeasureTheory.setIntegral_congr_set polarCoordReal_symm_target_ae_eq_univ MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instIsAddHaarMeasureRealMixedSpaceVolume IsOpen.measurableSet Prod.opensMeasurableSpace Pi.opensMeasurableSpace BorelSpace.opensMeasurable OpenPartialHomeomorph.open_target HasFDerivAt.hasFDerivWithinAt hasFDerivAt_polarCoordReal_symm OpenPartialHomeomorph.injOn MeasureTheory.setIntegral_congr_fun det_fderivPolarCoordRealSymm Finset.abs_prod Real.instIsStrictOrderedRing Finset.prod_congr
integral_comp_polarCoord_symm 📖	mathematical	—	MeasureTheory.integral realMixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target mixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarCoord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Finset.prod Real.instCommMonoid Finset.univ OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace	—	Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.MeasurePreserving.integral_comp volume_preserving_mixedSpaceToRealMixedSpace_symm Homeomorph.measurableEmbedding Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable secondCountable_of_proper Complex.instProperSpace integral_comp_polarCoordReal_symm polarCoord_target_eq_polarCoordReal_target polarCoord_symm_eq
integral_comp_polarSpaceCoord_symm 📖	mathematical	—	MeasureTheory.integral polarSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex Subtype.fintype MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target mixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarSpaceCoord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Finset.prod Real.instCommMonoid Finset.univ OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace	—	Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.MeasurePreserving.setIntegral_preimage_emb volume_preserving_homeoRealMixedSpacePolarSpace Homeomorph.measurableEmbedding Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable integral_comp_polarCoord_symm polarSpaceCoord_target Homeomorph.image_eq_preimage_symm Homeomorph.preimage_image polarCoord_target homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal Finset.prod_congr homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex
lintegral_comp_polarCoordReal_symm 📖	mathematical	—	MeasureTheory.lintegral realMixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoordReal ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Finset.prod CommSemiring.toCommMonoid Finset.univ ENNReal.ofReal OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	MeasureTheory.setLIntegral_univ MeasureTheory.setLIntegral_congr polarCoordReal_symm_target_ae_eq_univ MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul Module.Finite.prod FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable instIsAddHaarMeasureRealMixedSpaceVolume IsOpen.measurableSet Prod.opensMeasurableSpace Pi.opensMeasurableSpace BorelSpace.opensMeasurable OpenPartialHomeomorph.open_target HasFDerivAt.hasFDerivWithinAt hasFDerivAt_polarCoordReal_symm OpenPartialHomeomorph.injOn MeasureTheory.setLIntegral_congr_fun det_fderivPolarCoordRealSymm Finset.abs_prod Real.instIsStrictOrderedRing ENNReal.ofReal_prod_of_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.prod_congr
lintegral_comp_polarCoord_symm 📖	mathematical	—	MeasureTheory.lintegral realMixedSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target mixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarCoord ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Finset.prod CommSemiring.toCommMonoid Finset.univ ENNReal.ofReal OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace	—	Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.MeasurePreserving.lintegral_comp_emb volume_preserving_mixedSpaceToRealMixedSpace_symm Homeomorph.measurableEmbedding Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable secondCountable_of_proper Complex.instProperSpace lintegral_comp_polarCoordReal_symm polarCoord_target_eq_polarCoordReal_target polarCoord_symm_eq
lintegral_comp_polarSpaceCoord_symm 📖	mathematical	—	MeasureTheory.lintegral polarSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex Subtype.fintype MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target mixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace.IsReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarSpaceCoord ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Finset.prod CommSemiring.toCommMonoid Finset.univ ENNReal.ofReal OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.measurableSpace Complex.borelSpace	—	Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb volume_preserving_homeoRealMixedSpacePolarSpace Homeomorph.measurableEmbedding Prod.borelSpace Pi.borelSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable lintegral_comp_polarCoord_symm polarSpaceCoord_target Homeomorph.image_eq_preimage_symm Homeomorph.preimage_image polarCoord_target homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal Finset.prod_congr homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex
measurable_polarCoordReal_symm 📖	mathematical	—	Measurable realMixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex OpenPartialHomeomorph.toFun' instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm polarCoordReal	—	Measurable.prodMk measurable_fst Measurable.comp measurable_pi_lambda Continuous.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Prod.borelSpace continuous_polarCoord_symm measurable_pi_apply measurable_snd
measurable_polarCoord_symm 📖	mathematical	—	Measurable realMixedSpace mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace OpenPartialHomeomorph.toFun' instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarCoord	—	polarCoord_symm_eq Measurable.comp Homeomorph.measurable Prod.opensMeasurableSpace Pi.opensMeasurableSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace TopologicalSpace.instSecondCountableTopologyProd secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable Prod.borelSpace Pi.borelSpace secondCountable_of_proper Complex.instProperSpace Complex.borelSpace measurable_polarCoordReal_symm
measurable_polarSpaceCoord_symm 📖	mathematical	—	Measurable polarSpace mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace Real Real.measurableSpace NumberField.InfinitePlace.IsComplex NumberField.InfinitePlace.IsReal Complex Complex.measurableSpace OpenPartialHomeomorph.toFun' instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarSpaceCoord	—	polarSpaceCoord.eq_1 OpenPartialHomeomorph.transHomeomorph_symm_apply Measurable.comp measurable_polarCoord_symm Homeomorph.measurable Prod.opensMeasurableSpace Pi.opensMeasurableSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Subtype.countable secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable Prod.borelSpace Pi.borelSpace TopologicalSpace.instSecondCountableTopologyProd
mixedSpaceToRealMixedSpace_apply 📖	mathematical	—	DFunLike.coe Homeomorph mixedSpace realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField EquivLike.toFunLike Homeomorph.instEquivLike mixedSpaceToRealMixedSpace Equiv Equiv.instEquivLike Complex.equivRealProd	—	—
normAtComplexPlaces_polarSpaceCoord_symm 📖	mathematical	—	normAtComplexPlaces OpenPartialHomeomorph.toFun' polarSpace mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex NumberField.InfinitePlace.IsReal Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarSpaceCoord DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring realSpace Pi.addCommMonoid Real.instAddCommMonoid Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Prod.instModule instInnerProductSpaceRealComplex ContinuousLinearMap.funLike mixedSpaceOfRealSpace	—	NumberField.InfinitePlace.isReal_or_isComplex normAtComplexPlaces_apply_isReal normAtComplexPlaces_apply_isComplex Complex.polarCoord_symm_apply Complex.ofReal_cos Complex.ofReal_sin Complex.norm_mul Complex.norm_real Complex.norm_cos_add_sin_mul_I mul_one
normAtPlace_polarCoord_symm_of_isComplex 📖	mathematical	NumberField.InfinitePlace.IsComplex	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace OpenPartialHomeomorph.toFun' realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarCoord Norm.norm Real.norm	—	normAtPlace_apply_of_isComplex Complex.polarCoord_symm_apply Complex.ofReal_cos Complex.ofReal_sin Complex.norm_mul Complex.norm_real Complex.norm_cos_add_sin_mul_I mul_one
normAtPlace_polarCoord_symm_of_isReal 📖	mathematical	NumberField.InfinitePlace.IsReal	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace OpenPartialHomeomorph.toFun' realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarCoord Norm.norm Real.norm	—	normAtPlace_apply_of_isReal
polarCoordReal_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex polarCoordReal Pi.map polarCoord	—	—
polarCoordReal_source 📖	mathematical	—	PartialEquiv.source realMixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex polarCoordReal SProd.sprod Set Set.instSProd Set.univ Set.pi polarCoord	—	—
polarCoordReal_symm_target_ae_eq_univ 📖	mathematical	—	Filter.EventuallyEq realMixedSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real Real.measureSpace NumberField.InfinitePlace.IsComplex MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume Set.image OpenPartialHomeomorph.toFun' instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm polarCoordReal PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv Set.univ	—	MeasureTheory.Measure.instOuterMeasureClass Set.univ_prod_univ MeasureTheory.Measure.volume_eq_prod OpenPartialHomeomorph.symm_image_target_eq_source polarCoordReal_source Set.piMap_image_univ_pi MeasureTheory.Measure.set_prod_ae_eq Filter.EventuallyEq.rfl pi_polarCoord_symm_target_ae_eq_univ
polarCoordReal_target 📖	mathematical	—	PartialEquiv.target realMixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex polarCoordReal SProd.sprod Set Set.instSProd Set.univ Set.pi Set.Ioi Real.instPreorder Real.instZero Set.Ioo Real.instNeg Real.pi	—	—
polarCoord_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' mixedSpace realMixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarCoord Pi.map Complex.polarCoord	—	—
polarCoord_source 📖	mathematical	—	PartialEquiv.source mixedSpace realMixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarCoord SProd.sprod Set Set.instSProd Set.univ Set.pi Complex.polarCoord	—	—
polarCoord_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' realMixedSpace mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarCoord Pi.map Complex.polarCoord	—	—
polarCoord_symm_eq 📖	mathematical	—	OpenPartialHomeomorph.toFun' realMixedSpace mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarCoord DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm mixedSpaceToRealMixedSpace polarCoordReal	—	—
polarCoord_target 📖	mathematical	—	PartialEquiv.target mixedSpace realMixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarCoord SProd.sprod Set Set.instSProd Set.univ Set.pi Complex.polarCoord	—	—
polarCoord_target_eq_polarCoordReal_target 📖	mathematical	—	PartialEquiv.target mixedSpace realMixedSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarCoord polarCoordReal	—	—
polarSpaceCoord_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' mixedSpace polarSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarSpaceCoord DFunLike.coe Homeomorph realMixedSpace EquivLike.toFunLike Homeomorph.instEquivLike homeoRealMixedSpacePolarSpace Pi.map Complex.polarCoord	—	—
polarSpaceCoord_source 📖	mathematical	—	PartialEquiv.source mixedSpace polarSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarSpaceCoord SProd.sprod Set Set.instSProd Set.univ Set.pi Complex.polarCoord	—	—
polarSpaceCoord_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' polarSpace mixedSpace instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex NumberField.InfinitePlace.IsReal Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField OpenPartialHomeomorph.symm polarSpaceCoord Pi.map Complex.polarCoord	—	—
polarSpaceCoord_target 📖	mathematical	—	PartialEquiv.target mixedSpace polarSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarSpaceCoord Set.preimage realMixedSpace DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeoRealMixedSpacePolarSpace SProd.sprod Set Set.instSProd Set.univ Set.pi Complex.polarCoord	—	—
polarSpaceCoord_target' 📖	mathematical	—	PartialEquiv.target mixedSpace polarSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Pi.topologicalSpace NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NumberField.InfinitePlace.IsComplex Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField polarSpaceCoord SProd.sprod Set Set.instSProd Set.pi Set.univ Set.Ioo Real.instPreorder Real.instNeg Real.pi	—	Set.ext
volume_eq_two_pi_pow_mul_integral 📖	mathematical	Set.preimage mixedSpace realSpace normAtComplexPlaces Set.image MeasurableSet Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofReal Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi NumberField.InfinitePlace.nrComplexPlaces MeasureTheory.lintegral MeasureTheory.Measure.restrict Finset.prod CommSemiring.toCommMonoid Finset.univ	—	Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat MeasureTheory.lintegral_indicator_one lintegral_comp_polarSpaceCoord_symm polarSpaceCoord_target' MeasureTheory.Measure.volume_eq_prod MeasureTheory.setLIntegral_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Measurable.aemeasurable Measurable.mul ENNReal.instMeasurableMul₂ Finset.measurable_prod Measurable.ennreal_ofReal Measurable.fun_comp measurable_pi_apply Measurable.fst measurable_id' Measurable.indicator measurable_const MeasurableSet.preimage measurable_polarSpaceCoord_symm Finset.prod_congr normAtComplexPlaces_polarSpaceCoord_symm MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply MeasurableSet.univ Set.univ_inter MeasureTheory.Measure.pi_pi Real.volume_Ioo sub_neg_eq_add Finset.prod_const mul_one MeasureTheory.lintegral_mul_const' instLawfulBCmpCompare_mathlib mul_comm MeasureTheory.setLIntegral_indicator ContinuousLinearMap.measurable Pi.opensMeasurableSpace Finite.to_countable Finite.of_fintype BorelSpace.opensMeasurable Prod.borelSpace Pi.borelSpace Subtype.countable PolishSpace.toSecondCountableTopology instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace secondCountable_of_proper Complex.instProperSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Complex.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable MeasureTheory.setLIntegral_congr MeasureTheory.ae_eq_set_inter MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.refl MeasureTheory.Measure.ae_eq_set_pi MeasureTheory.ae_eq_rfl MeasureTheory.Ioi_ae_eq_Ici Real.noAtoms_volume
volume_eq_two_pow_mul_two_pi_pow_mul_integral 📖	mathematical	Set.preimage mixedSpace realSpace normAtAllPlaces Set.image MeasurableSet Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat NumberField.InfinitePlace.nrRealPlaces ENNReal.ofReal Real.instMul Real.instNatCast Real.pi NumberField.InfinitePlace.nrComplexPlaces MeasureTheory.lintegral MeasureTheory.Measure.restrict Finset.prod CommSemiring.toCommMonoid Finset.univ	—	normAtAllPlaces_norm_at_real_places subset_antisymm Set.instAntisymmSubset Set.mem_preimage normAtAllPlaces_eq_of_normAtComplexPlaces_eq Set.mem_image_of_mem Set.inter_subset_left normAtComplexPlaces_apply_isReal Set.subset_preimage_image Complex.instFiniteDimensionalReal Complex.borelSpace Nat.instAtLeastTwoHAddOfNat volume_eq_two_pow_mul_volume_plusPart volume_eq_two_pi_pow_mul_integral measurableSet_plusPart mul_assoc MeasureTheory.setLIntegral_congr MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.inter_ae_eq_left_of_ae_eq_univ MeasureTheory.ae_eq_univ MeasureTheory.measure_iUnion_null_iff Subtype.countable Finite.to_countable Finite.of_fintype Set.ext realSpace.volume_eq_zero Set.compl_iInter
volume_preserving_homeoRealMixedSpacePolarSpace 📖	mathematical	—	MeasureTheory.MeasurePreserving realMixedSpace polarSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex DFunLike.coe Homeomorph instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike homeoRealMixedSpacePolarSpace MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace	—	MeasureTheory.MeasurePreserving.trans MeasureTheory.MeasurePreserving.prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.instSigmaFiniteProdVolume MeasureTheory.MeasurePreserving.id MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow MeasureTheory.MeasurePreserving.symm MeasureTheory.volume_preserving_prodAssoc MeasureTheory.Measure.prod.instSFinite MeasureTheory.volume_preserving_arrowCongr' MeasureTheory.Measure.instSFiniteProdVolume MeasureTheory.volume_preserving_piEquivPiSubtypeProd
volume_preserving_mixedSpaceToRealMixedSpace_symm 📖	mathematical	—	MeasureTheory.MeasurePreserving realMixedSpace mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace DFunLike.coe Homeomorph instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm mixedSpaceToRealMixedSpace MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.prod.measureSpace MeasureTheory.MeasureSpace.pi Subtype.fintype NumberField.InfinitePlace.NumberField.InfinitePlace.fintype Real.measureSpace measureSpaceOfInnerProductSpace Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Complex.borelSpace	—	MeasureTheory.MeasurePreserving.prod Complex.instFiniteDimensionalReal Complex.borelSpace MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.instSigmaFiniteProdVolume RingHomInvPair.ids MeasureTheory.MeasurePreserving.id MeasureTheory.volume_preserving_pi SeminormedAddCommGroup.toIsTopologicalAddGroup secondCountable_of_proper Complex.instProperSpace MeasureTheory.MeasurePreserving.symm Complex.volume_preserving_equiv_real_prod

---

← Back to Index