Basic

📁 Source: Mathlib/Analysis/Complex/UnitDisc/Basic.lean

Statistics

Metric	Count
Definitions `UnitDisc`, `casesOn`, `conj`, `im`, `instCoe`, `instCommSemigroup`, `instHasDistribNeg`, `instInhabited`, `instInvolutiveStar`, `instMulActionCircle`, `instMulActionClosedBall`, `instPowPNat`, `instSemigroupWithZero`, `instStar`, `instStarMul`, `mk`, `re`, `term𝔻`, `instTopologicalSpaceUnitDisc`	19
Theorems `casesOn_mk`, `coe_circle_smul`, `coe_closedBall_smul`, `coe_conj`, `coe_eq_zero`, `coe_inj`, `coe_injective`, `coe_injective_iff`, `coe_mk`, `coe_mul`, `coe_ne_neg_one`, `coe_ne_one`, `coe_neg`, `coe_pow`, `coe_smul_circle`, `coe_smul_closedBall`, `coe_star`, `coe_zero`, `conj_conj`, `conj_mul`, `conj_neg`, `continuous_coe`, `continuous_pow`, `exists`, `forall`, `im_coe`, `im_conj`, `im_neg`, `im_star`, `im_zero`, `instCanLiftCoeLtRealNormOfNat`, `instIsCancelMulZero`, `instIsScalarTower_circle`, `instIsScalarTower_circle_circle`, `instIsScalarTower_closedBall`, `instIsScalarTower_closedBall_closedBall`, `instPNatPowAssoc`, `instSMulCommClass_circle_closedBall`, `instSMulCommClass_circle_left`, `instSMulCommClass_circle_right`, `instSMulCommClass_closedBall_circle`, `instSMulCommClass_closedBall_left`, `instSMulCommClass_closedBall_right`, `isEmbedding_coe`, `mk_coe`, `mk_eq_zero`, `mk_inj`, `mk_neg`, `mk_zero`, `normSq_lt_one`, `norm_lt_one`, `norm_ne_one`, `one_add_coe_ne_zero`, `pow_eq_zero`, `re_coe`, `re_conj`, `re_neg`, `re_star`, `re_zero`, `sq_norm_lt_one`, `star_eq_zero`, `star_neg`, `star_zero`, `tendsto_pow_atTop_nhds_zero`	64
Total	83

Complex

Definitions

Name	Category	Theorems
`UnitDisc` 📖	CompOp	47 math math: `UnitDisc.coe_eq_zero`, `UnitDisc.instIsScalarTower_circle`, `UnitDisc.instSMulCommClass_closedBall_circle`, `UnitDisc.instSMulCommClass_closedBall_left`, `UnitDisc.conj_neg`, `UnitDisc.coe_neg`, `UnitDisc.im_neg`, `UnitDisc.im_star`, `UnitDisc.coe_smul_circle`, `UnitDisc.instIsScalarTower_circle_circle`, `UnitDisc.coe_conj`, `UnitDisc.instSMulCommClass_circle_left`, `UnitDisc.conj_mul`, `UnitDisc.coe_pow`, `UnitDisc.isEmbedding_coe`, `UnitDisc.coe_closedBall_smul`, `UnitDisc.instCanLiftCoeLtRealNormOfNat`, `UnitDisc.re_neg`, `UnitDisc.im_conj`, `UnitDisc.instSMulCommClass_closedBall_right`, `UnitDisc.instIsScalarTower_closedBall`, `UnitDisc.instIsCancelMulZero`, `UnitDisc.pow_eq_zero`, `UnitDisc.mk_neg`, `UnitDisc.coe_mul`, `UnitDisc.im_zero`, `UnitDisc.coe_smul_closedBall`, `UnitDisc.re_star`, `UnitDisc.instSMulCommClass_circle_right`, `UnitDisc.mk_zero`, `UnitDisc.mk_eq_zero`, `UnitDisc.coe_injective`, `UnitDisc.continuous_coe`, `UnitDisc.re_zero`, `UnitDisc.coe_zero`, `UnitDisc.re_conj`, `UnitDisc.conj_conj`, `UnitDisc.tendsto_pow_atTop_nhds_zero`, `UnitDisc.instSMulCommClass_circle_closedBall`, `UnitDisc.star_neg`, `UnitDisc.star_eq_zero`, `UnitDisc.star_zero`, `UnitDisc.instPNatPowAssoc`, `UnitDisc.coe_star`, `UnitDisc.instIsScalarTower_closedBall_closedBall`, `UnitDisc.coe_circle_smul`, `UnitDisc.continuous_pow`
`instTopologicalSpaceUnitDisc` 📖	CompOp	4 math math: `UnitDisc.isEmbedding_coe`, `UnitDisc.continuous_coe`, `UnitDisc.tendsto_pow_atTop_nhds_zero`, `UnitDisc.continuous_pow`

Complex.UnitDisc

Definitions

Name	Category	Theorems
`casesOn` 📖	CompOp	—
`conj` 📖	CompOp	—
`im` 📖	CompOp	5 math math: `im_neg`, `im_star`, `im_conj`, `im_zero`, `im_coe`
`instCoe` 📖	CompOp	—
`instCommSemigroup` 📖	CompOp	—
`instHasDistribNeg` 📖	CompOp	6 math math: `conj_neg`, `coe_neg`, `im_neg`, `re_neg`, `mk_neg`, `star_neg`
`instInhabited` 📖	CompOp	—
`instInvolutiveStar` 📖	CompOp	—
`instMulActionCircle` 📖	CompOp	8 math math: `instIsScalarTower_circle`, `instSMulCommClass_closedBall_circle`, `coe_smul_circle`, `instIsScalarTower_circle_circle`, `instSMulCommClass_circle_left`, `instSMulCommClass_circle_right`, `instSMulCommClass_circle_closedBall`, `coe_circle_smul`
`instMulActionClosedBall` 📖	CompOp	8 math math: `instSMulCommClass_closedBall_circle`, `instSMulCommClass_closedBall_left`, `coe_closedBall_smul`, `instSMulCommClass_closedBall_right`, `instIsScalarTower_closedBall`, `coe_smul_closedBall`, `instSMulCommClass_circle_closedBall`, `instIsScalarTower_closedBall_closedBall`
`instPowPNat` 📖	CompOp	5 math math: `coe_pow`, `pow_eq_zero`, `tendsto_pow_atTop_nhds_zero`, `instPNatPowAssoc`, `continuous_pow`
`instSemigroupWithZero` 📖	CompOp	26 math math: `coe_eq_zero`, `instIsScalarTower_circle`, `instSMulCommClass_closedBall_left`, `conj_neg`, `coe_neg`, `im_neg`, `instSMulCommClass_circle_left`, `conj_mul`, `re_neg`, `instSMulCommClass_closedBall_right`, `instIsScalarTower_closedBall`, `instIsCancelMulZero`, `pow_eq_zero`, `mk_neg`, `coe_mul`, `im_zero`, `instSMulCommClass_circle_right`, `mk_zero`, `mk_eq_zero`, `re_zero`, `coe_zero`, `tendsto_pow_atTop_nhds_zero`, `star_neg`, `star_eq_zero`, `star_zero`, `instPNatPowAssoc`
`instStar` 📖	CompOp	12 math math: `conj_neg`, `im_star`, `coe_conj`, `conj_mul`, `im_conj`, `re_star`, `re_conj`, `conj_conj`, `star_neg`, `star_eq_zero`, `star_zero`, `coe_star`
`instStarMul` 📖	CompOp	—
`mk` 📖	CompOp	—
`re` 📖	CompOp	5 math math: `re_neg`, `re_coe`, `re_star`, `re_zero`, `re_conj`
`term𝔻` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`casesOn_mk` 📖	—	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Real.instOne`	—	—	—
`coe_circle_smul` 📖	mathematical	—	`coe` `Circle` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `instMulActionCircle` `Complex` `Complex.instMul` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	—
`coe_closedBall_smul` 📖	mathematical	—	`coe` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `MulAction.toSemigroupAction` `instMulActionClosedBall` `Complex.instMul` `Set` `Set.instMembership`	—	`NormedDivisionRing.to_normOneClass`
`coe_conj` 📖	mathematical	—	`coe` `Star.star` `Complex.UnitDisc` `instStar` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing`	—	`coe_star`
`coe_eq_zero` 📖	mathematical	—	`coe` `Complex` `Complex.instZero` `Complex.UnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	`coe_injective` `coe_zero`
`coe_inj` 📖	mathematical	—	`coe`	—	—
`coe_injective` 📖	mathematical	—	`Complex.UnitDisc` `Complex` `coe`	—	`Subtype.coe_injective`
`coe_injective_iff` 📖	mathematical	—	`coe`	—	`coe_injective`
`coe_mk` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Real.instOne`	`coe`	—	—
`coe_mul` 📖	mathematical	—	`coe` `Complex.UnitDisc` `MulZeroClass.toMul` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `Complex` `Complex.instMul`	—	—
`coe_ne_neg_one` 📖	—	—	—	—	`norm_neg` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `norm_ne_one`
`coe_ne_one` 📖	—	—	—	—	`CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `norm_ne_one`
`coe_neg` 📖	mathematical	—	`coe` `Complex.UnitDisc` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instHasDistribNeg` `Complex` `Complex.instNeg`	—	—
`coe_pow` 📖	mathematical	—	`coe` `Complex.UnitDisc` `PNat` `instPowPNat` `Complex` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `PNat.val`	—	—
`coe_smul_circle` 📖	mathematical	—	`coe` `Circle` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `instMulActionCircle` `Complex` `Complex.instMul` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere`	—	`coe_circle_smul`
`coe_smul_closedBall` 📖	mathematical	—	`coe` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `MulAction.toSemigroupAction` `instMulActionClosedBall` `Complex.instMul` `Set` `Set.instMembership`	—	`coe_closedBall_smul`
`coe_star` 📖	mathematical	—	`coe` `Star.star` `Complex.UnitDisc` `instStar` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing`	—	—
`coe_zero` 📖	mathematical	—	`coe` `Complex.UnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `Complex` `Complex.instZero`	—	—
`conj_conj` 📖	mathematical	—	`Star.star` `Complex.UnitDisc` `instStar`	—	`star_star`
`conj_mul` 📖	mathematical	—	`Star.star` `Complex.UnitDisc` `instStar` `MulZeroClass.toMul` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	`star_mul'`
`conj_neg` 📖	mathematical	—	`Star.star` `Complex.UnitDisc` `instStar` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instHasDistribNeg`	—	`star_neg`
`continuous_coe` 📖	mathematical	—	`Continuous` `Complex.UnitDisc` `Complex` `Complex.instTopologicalSpaceUnitDisc` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe`	—	`Topology.IsEmbedding.continuous` `isEmbedding_coe`
`continuous_pow` 📖	mathematical	—	`Continuous` `Complex.UnitDisc` `Complex.instTopologicalSpaceUnitDisc` `PNat` `instPowPNat`	—	`Topology.IsEmbedding.continuous_iff` `isEmbedding_coe` `Continuous.comp'` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_id'` `continuous_coe`
`exists` 📖	—	—	—	—	`norm_lt_one`
`forall` 📖	—	—	—	—	`norm_lt_one`
`im_coe` 📖	mathematical	—	`Complex.im` `coe` `im`	—	—
`im_conj` 📖	mathematical	—	`im` `Star.star` `Complex.UnitDisc` `instStar` `Real` `Real.instNeg`	—	`im_star`
`im_neg` 📖	mathematical	—	`im` `Complex.UnitDisc` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instHasDistribNeg` `Real` `Real.instNeg`	—	—
`im_star` 📖	mathematical	—	`im` `Star.star` `Complex.UnitDisc` `instStar` `Real` `Real.instNeg`	—	—
`im_zero` 📖	mathematical	—	`im` `Complex.UnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `Real` `Real.instZero`	—	—
`instCanLiftCoeLtRealNormOfNat` 📖	mathematical	—	`CanLift` `Complex` `Complex.UnitDisc` `coe` `Real` `Real.instLT` `Norm.norm` `Complex.instNorm` `Real.instOne`	—	—
`instIsCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `Complex.UnitDisc` `MulZeroClass.toMul` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `MulZeroClass.toZero`	—	`Metric.unitBall.instIsCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain`
`instIsScalarTower_circle` 📖	mathematical	—	`IsScalarTower` `Circle` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `instMulActionCircle` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`isScalarTower_sphere_ball_ball`
`instIsScalarTower_circle_circle` 📖	mathematical	—	`IsScalarTower` `Circle` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `instMulActionCircle`	—	`isScalarTower_sphere_sphere_ball` `IsScalarTower.right`
`instIsScalarTower_closedBall` 📖	mathematical	—	`IsScalarTower` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `MulAction.toSemigroupAction` `instMulActionClosedBall` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`isScalarTower_closedBall_ball_ball`
`instIsScalarTower_closedBall_closedBall` 📖	mathematical	—	`IsScalarTower` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Complex.UnitDisc` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Metric.unitClosedBall.instMonoidWithZero` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `MulAction.toSemigroupAction` `instMulActionClosedBall`	—	`isScalarTower_closedBall_closedBall_ball` `IsScalarTower.right`
`instPNatPowAssoc` 📖	mathematical	—	`PNatPowAssoc` `Complex.UnitDisc` `MulZeroClass.toMul` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instPowPNat`	—	`pow_add` `pow_one`
`instSMulCommClass_circle_closedBall` 📖	mathematical	—	`SMulCommClass` `Circle` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `instMulActionCircle` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `instMulActionClosedBall`	—	`instSMulCommClass_sphere_closedBall_ball` `Algebra.to_smulCommClass`
`instSMulCommClass_circle_left` 📖	mathematical	—	`SMulCommClass` `Circle` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `instMulActionCircle` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`instSMulCommClass_sphere_ball_ball`
`instSMulCommClass_circle_right` 📖	mathematical	—	`SMulCommClass` `Complex.UnitDisc` `Circle` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `MulAction.toSemigroupAction` `instMulActionCircle`	—	`SMulCommClass.symm` `instSMulCommClass_circle_left`
`instSMulCommClass_closedBall_circle` 📖	mathematical	—	`SMulCommClass` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Circle` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `MulAction.toSemigroupAction` `instMulActionClosedBall` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `instMulActionCircle`	—	`SMulCommClass.symm` `NormedDivisionRing.to_normOneClass` `instSMulCommClass_circle_closedBall`
`instSMulCommClass_closedBall_left` 📖	mathematical	—	`SMulCommClass` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `Complex.UnitDisc` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `MulAction.toSemigroupAction` `instMulActionClosedBall` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`NormedDivisionRing.to_normOneClass` `mul_left_comm`
`instSMulCommClass_closedBall_right` 📖	mathematical	—	`SMulCommClass` `Complex.UnitDisc` `Set.Elem` `Complex` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instZero` `Real` `Real.instOne` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Metric.unitClosedBall.instMonoid` `NormedDivisionRing.to_normOneClass` `NormedField.toNormedDivisionRing` `MulAction.toSemigroupAction` `instMulActionClosedBall`	—	`SMulCommClass.symm` `NormedDivisionRing.to_normOneClass` `instSMulCommClass_closedBall_left`
`isEmbedding_coe` 📖	mathematical	—	`Topology.IsEmbedding` `Complex.UnitDisc` `Complex` `Complex.instTopologicalSpaceUnitDisc` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `coe`	—	`Topology.IsEmbedding.subtypeVal`
`mk_coe` 📖	—	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `coe` `Real.instOne` `norm_lt_one`	—	—	—
`mk_eq_zero` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Real.instOne`	`Complex.UnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `Complex.instZero`	—	—
`mk_inj` 📖	—	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Real.instOne`	—	—	—
`mk_neg` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instNeg` `Real.instOne`	`Complex.UnitDisc` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instHasDistribNeg` `SeminormedAddGroup.toNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SeminormedAddGroup.toAddGroup` `norm_neg`	—	—
`mk_zero` 📖	mathematical	—	`Complex` `Complex.instZero` `Complex.UnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	—
`normSq_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `DFunLike.coe` `MonoidWithZeroHom` `Complex` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `Real.semiring` `MonoidWithZeroHom.funLike` `Complex.normSq` `coe` `Real.instOne`	—	`Complex.norm_mul_self_eq_normSq` `sq` `sq_norm_lt_one`
`norm_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `Complex` `Complex.instNorm` `coe` `Real.instOne`	—	`mem_ball_zero_iff`
`norm_ne_one` 📖	—	—	—	—	`LT.lt.ne` `norm_lt_one`
`one_add_coe_ne_zero` 📖	—	—	—	—	`neg_eq_iff_add_eq_zero` `coe_ne_neg_one`
`pow_eq_zero` 📖	mathematical	—	`Complex.UnitDisc` `PNat` `instPowPNat` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	`coe_pow` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`re_coe` 📖	mathematical	—	`Complex.re` `coe` `re`	—	—
`re_conj` 📖	mathematical	—	`re` `Star.star` `Complex.UnitDisc` `instStar`	—	`re_star`
`re_neg` 📖	mathematical	—	`re` `Complex.UnitDisc` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instHasDistribNeg` `Real` `Real.instNeg`	—	—
`re_star` 📖	mathematical	—	`re` `Star.star` `Complex.UnitDisc` `instStar`	—	—
`re_zero` 📖	mathematical	—	`re` `Complex.UnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `Real` `Real.instZero`	—	—
`sq_norm_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `Complex` `Complex.instNorm` `coe` `Real.instOne`	—	`sq_lt_one_iff_abs_lt_one` `Real.instIsStrictOrderedRing` `abs_norm` `norm_lt_one`
`star_eq_zero` 📖	mathematical	—	`Star.star` `Complex.UnitDisc` `instStar` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	`Complex.instNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`star_neg` 📖	mathematical	—	`Star.star` `Complex.UnitDisc` `instStar` `NegZeroClass.toNeg` `MulZeroClass.negZeroClass` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero` `instHasDistribNeg`	—	—
`star_zero` 📖	mathematical	—	`Star.star` `Complex.UnitDisc` `instStar` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	—
`tendsto_pow_atTop_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `PNat` `Complex.UnitDisc` `instPowPNat` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `nhds` `Complex.instTopologicalSpaceUnitDisc` `MulZeroClass.toZero` `SemigroupWithZero.toMulZeroClass` `instSemigroupWithZero`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding_coe` `Filter.Tendsto.comp` `tendsto_pow_atTop_nhds_zero_iff_norm_lt_one` `NormedDivisionRing.toNormMulClass` `norm_lt_one` `tendsto_PNat_val_atTop_atTop`

---

← Back to Index