Documentation Verification Report

Complex

📁 Source: Mathlib/MeasureTheory/Measure/Complex.lean

Statistics

Metric	Count
Definitions `ComplexMeasure`, `equivSignedMeasure`, `equivSignedMeasureₗ`, `im`, `re`, `toComplexMeasure`	6
Theorems `absolutelyContinuous_ennreal_iff`, `equivSignedMeasure_apply`, `equivSignedMeasure_symm_apply`, `equivSignedMeasureₗ_apply`, `equivSignedMeasureₗ_symm_apply`, `im_apply`, `re_apply`, `toComplexMeasure_to_signedMeasure`, `im_toComplexMeasure`, `re_toComplexMeasure`, `toComplexMeasure_apply`, `toComplexMeasure_apply_im`, `toComplexMeasure_apply_re`	13
Total	19

MeasureTheory

Definitions

Name	Category	Theorems
`ComplexMeasure` 📖	CompOp	13 math math: `ComplexMeasure.equivSignedMeasure_symm_apply`, `ComplexMeasure.HaveLebesgueDecomposition.imPart`, `ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq`, `ComplexMeasure.equivSignedMeasure_apply`, `SignedMeasure.re_toComplexMeasure`, `ComplexMeasure.HaveLebesgueDecomposition.rePart`, `ComplexMeasure.im_apply`, `ComplexMeasure.equivSignedMeasureₗ_symm_apply`, `ComplexMeasure.absolutelyContinuous_ennreal_iff`, `ComplexMeasure.re_apply`, `ComplexMeasure.toComplexMeasure_to_signedMeasure`, `ComplexMeasure.equivSignedMeasureₗ_apply`, `SignedMeasure.im_toComplexMeasure`

MeasureTheory.ComplexMeasure

Definitions

Name	Category	Theorems
`equivSignedMeasure` 📖	CompOp	4 math math: `equivSignedMeasure_symm_apply`, `equivSignedMeasure_apply`, `equivSignedMeasureₗ_symm_apply`, `equivSignedMeasureₗ_apply`
`equivSignedMeasureₗ` 📖	CompOp	2 math math: `equivSignedMeasureₗ_symm_apply`, `equivSignedMeasureₗ_apply`
`im` 📖	CompOp	6 math math: `HaveLebesgueDecomposition.imPart`, `equivSignedMeasure_apply`, `im_apply`, `absolutelyContinuous_ennreal_iff`, `toComplexMeasure_to_signedMeasure`, `MeasureTheory.SignedMeasure.im_toComplexMeasure`
`re` 📖	CompOp	6 math math: `equivSignedMeasure_apply`, `MeasureTheory.SignedMeasure.re_toComplexMeasure`, `HaveLebesgueDecomposition.rePart`, `absolutelyContinuous_ennreal_iff`, `re_apply`, `toComplexMeasure_to_signedMeasure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_ennreal_iff` 📖	mathematical	—	`MeasureTheory.VectorMeasure.AbsolutelyContinuous` `Complex` `ENNReal` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZero` `Complex.instZero` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `re` `im`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `Complex.re_add_im` `MulZeroClass.zero_mul` `add_zero`
`equivSignedMeasure_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSignedMeasure` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `Real.normedCommRing` `LinearMap.instFunLike` `re` `im`	—	—
`equivSignedMeasure_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MeasureTheory.SignedMeasure` `MeasureTheory.ComplexMeasure` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSignedMeasure` `MeasureTheory.SignedMeasure.toComplexMeasure`	—	—
`equivSignedMeasureₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Prod.instAddCommMonoid` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `Complex.instModule` `Prod.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `equivSignedMeasureₗ` `Equiv.toFun` `equivSignedMeasure`	—	`RingHomInvPair.ids` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal`
`equivSignedMeasureₗ_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MeasureTheory.SignedMeasure` `MeasureTheory.ComplexMeasure` `Prod.instAddCommMonoid` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Prod.instModule` `MeasureTheory.VectorMeasure.instModule` `Complex.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `equivSignedMeasureₗ` `Equiv.invFun` `equivSignedMeasure`	—	`RingHomInvPair.ids` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`im_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZero` `Complex.instZero` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `im` `MeasureTheory.VectorMeasure.mapRange` `LinearMap.toAddMonoidHom` `Complex.imLm` `Complex.continuous_im`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul`
`re_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZero` `Complex.instZero` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `re` `MeasureTheory.VectorMeasure.mapRange` `LinearMap.toAddMonoidHom` `Complex.reLm` `Complex.continuous_re`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul`
`toComplexMeasure_to_signedMeasure` 📖	mathematical	—	`MeasureTheory.SignedMeasure.toComplexMeasure` `DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZero` `Complex.instZero` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `re` `im`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul`

MeasureTheory.SignedMeasure

Definitions

Name	Category	Theorems
`toComplexMeasure` 📖	CompOp	7 math math: `MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply`, `toComplexMeasure_apply`, `re_toComplexMeasure`, `toComplexMeasure_apply_re`, `toComplexMeasure_apply_im`, `MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure`, `im_toComplexMeasure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`im_toComplexMeasure` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZero` `Complex.instZero` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `MeasureTheory.ComplexMeasure.im` `toComplexMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul`
`re_toComplexMeasure` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MeasureTheory.ComplexMeasure` `MeasureTheory.SignedMeasure` `MeasureTheory.VectorMeasure.instAddCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.normedCommRing` `instIsTopologicalRingReal` `MeasureTheory.VectorMeasure.instModule` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.instZero` `Complex.instZero` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LinearMap.instFunLike` `MeasureTheory.ComplexMeasure.re` `toComplexMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul`
`toComplexMeasure_apply` 📖	mathematical	—	`MeasureTheory.VectorMeasure.measureOf'` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `toComplexMeasure` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace`	—	—
`toComplexMeasure_apply_im` 📖	mathematical	—	`Complex.im` `MeasureTheory.VectorMeasure.measureOf'` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `toComplexMeasure` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace`	—	—
`toComplexMeasure_apply_re` 📖	mathematical	—	`Complex.re` `MeasureTheory.VectorMeasure.measureOf'` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `toComplexMeasure` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace`	—	—

---

← Back to Index