Documentation Verification Report

Convex

📁 Source: Mathlib/Analysis/Complex/Convex.lean

Statistics

Metric	Count
Definitions	0
Theorems `rectangle_subset`, `convexHull_reProdIm`, `instPathConnectedSpaceUnits`, `isConnected_of_lowerHalfPlane`, `isConnected_of_upperHalfPlane`, `rectangle_eq_convexHull`, `starConvex_ofReal_slitPlane`, `starConvex_one_slitPlane`, `starConvex_slitPlane`, `convex_halfSpace_im_ge`, `convex_halfSpace_im_gt`, `convex_halfSpace_im_le`, `convex_halfSpace_im_lt`, `convex_halfSpace_re_ge`, `convex_halfSpace_re_gt`, `convex_halfSpace_re_le`, `convex_halfSpace_re_lt`	17
Total	17

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexHull_reProdIm` 📖	mathematical	—	`DFunLike.coe` `ClosureOperator` `Set` `Complex` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `reProdIm` `Real.instAddCommMonoid` `Real.normedCommRing`	—	`RingHomInvPair.ids` `LinearMap.image_convexHull` `convexHull_prod` `Real.instIsStrictOrderedRing`
`instPathConnectedSpaceUnits` 📖	mathematical	—	`PathConnectedSpace` `Units` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Units.instTopologicalSpaceUnits` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	—	`isPathConnected_iff_pathConnectedSpace` `Set.ext` `IsPathConnected.union` `Convex.isPathConnected` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convex_halfSpace_im_gt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `convex_halfSpace_re_gt` `zero_add` `add_zero` `convex_halfSpace_im_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `convex_halfSpace_re_lt` `neg_zero` `zero_sub` `sub_zero` `IsTopologicalDivisionRing.toContinuousInv₀` `Function.Surjective.pathConnectedSpace` `Homeomorph.surjective` `Homeomorph.continuous`
`isConnected_of_lowerHalfPlane` 📖	mathematical	`Set` `Complex` `Set.instHasSubset` `setOf` `Real` `Real.instLT` `im` `Real.instLE`	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	—	`IsConnected.subset_closure` `Convex.isConnected` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convex_halfSpace_im_lt` `mul_one` `sub_self` `MulZeroClass.mul_zero` `add_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `closure_setOf_im_lt`
`isConnected_of_upperHalfPlane` 📖	mathematical	`Set` `Complex` `Set.instHasSubset` `setOf` `Real` `Real.instLT` `im` `Real.instLE`	`IsConnected` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	—	`IsConnected.subset_closure` `Convex.isConnected` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convex_halfSpace_im_gt` `mul_one` `add_zero` `MulZeroClass.mul_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `closure_setOf_lt_im`
`rectangle_eq_convexHull` 📖	mathematical	—	`Rectangle` `DFunLike.coe` `ClosureOperator` `Set` `Complex` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `Set.instInsert` `instAdd` `ofReal` `re` `instMul` `im` `I` `Set.instSingletonSet`	—	`Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Set.insert_prod` `Set.singleton_prod` `Set.image_pair` `Set.insert_union` `Set.image_insert_eq` `Set.image_singleton` `equivRealProd_symm_apply` `re_add_im`
`starConvex_ofReal_slitPlane` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StarConvex` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `instRCLike` `ofReal` `slitPlane`	—	`starConvex_slitPlane` `zero_lt_real`
`starConvex_one_slitPlane` 📖	mathematical	—	`StarConvex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `instRCLike` `instOne` `slitPlane`	—	`starConvex_slitPlane` `one_pos` `RCLike.toZeroLEOneClass` `NeZero.charZero_one` `instCharZero`
`starConvex_slitPlane` 📖	mathematical	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero`	`StarConvex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `instRCLike` `slitPlane`	—	`starConvex_compl_Iic` `RCLike.toIsOrderedAddMonoid` `RCLike.toIsStrictOrderedModule` `PosSMulStrictMono.toPosSMulReflectLT` `Real.instIsStrictOrderedRing` `instPosSMulStrictMono` `RCLike.toStarOrderedRing` `instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Real.instIsDomain` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `RCLike.toIsStrictOrderedRing` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `compl_Iic_zero`

Complex.Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rectangle_subset` 📖	mathematical	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `Set` `Set.instMembership` `Complex.instAdd` `Complex.ofReal` `Complex.re` `Complex.instMul` `Complex.im` `Complex.I`	`Set.instHasSubset` `Complex.Rectangle`	—	`Complex.rectangle_eq_convexHull` `convexHull_min`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convex_halfSpace_im_ge` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLE` `Complex.im`	—	`convex_halfSpace_ge` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Complex.add_im` `Complex.smul_im`
`convex_halfSpace_im_gt` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLT` `Complex.im`	—	`convex_halfSpace_gt` `Real.instIsOrderedCancelAddMonoid` `instPosSMulStrictMono` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Real.instIsDomain` `IsOrderedCancelAddMonoid.toIsCancelAdd` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Complex.add_im` `Complex.smul_im`
`convex_halfSpace_im_le` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLE` `Complex.im`	—	`convex_halfSpace_le` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Complex.add_im` `Complex.smul_im`
`convex_halfSpace_im_lt` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLT` `Complex.im`	—	`convex_halfSpace_lt` `Real.instIsOrderedCancelAddMonoid` `instPosSMulStrictMono` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Real.instIsDomain` `IsOrderedCancelAddMonoid.toIsCancelAdd` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Complex.add_im` `Complex.smul_im`
`convex_halfSpace_re_ge` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLE` `Complex.re`	—	`convex_halfSpace_ge` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Complex.add_re` `Complex.smul_re`
`convex_halfSpace_re_gt` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLT` `Complex.re`	—	`convex_halfSpace_gt` `Real.instIsOrderedCancelAddMonoid` `instPosSMulStrictMono` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Real.instIsDomain` `IsOrderedCancelAddMonoid.toIsCancelAdd` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Complex.add_re` `Complex.smul_re`
`convex_halfSpace_re_le` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLE` `Complex.re`	—	`convex_halfSpace_le` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Complex.add_re` `Complex.smul_re`
`convex_halfSpace_re_lt` 📖	mathematical	—	`Convex` `Real` `Complex` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `setOf` `Real.instLT` `Complex.re`	—	`convex_halfSpace_lt` `Real.instIsOrderedCancelAddMonoid` `instPosSMulStrictMono` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `Real.instIsDomain` `IsOrderedCancelAddMonoid.toIsCancelAdd` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Complex.add_re` `Complex.smul_re`

---

← Back to Index