Documentation Verification Report

CanonicalDecomposition

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

Statistics

Metric	Count
Definitions `canonicalFactor`	1
Theorems `analyticOnNhd_canonicalFactor`, `canonicalFactor_apply`, `canonicalFactor_apply_self`, `canonicalFactor_def`, `canonicalFactor_ne_zero`, `meromorphicNFOn_canonicalFactor`, `meromorphicOn_canonicalFactor`, `meromorphicOrderAt_canonicalFactor`, `norm_canonicalFactor_eval_circle_eq_one`	9
Total	10

Complex

Definitions

Name	Category	Theorems
`canonicalFactor` 📖	CompOp	8 math math: `meromorphicOrderAt_canonicalFactor`, `canonicalFactor_apply_self`, `meromorphicOn_canonicalFactor`, `canonicalFactor_def`, `norm_canonicalFactor_eval_circle_eq_one`, `analyticOnNhd_canonicalFactor`, `meromorphicNFOn_canonicalFactor`, `canonicalFactor_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticOnNhd_canonicalFactor` 📖	mathematical	—	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `canonicalFactor` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`canonicalFactor_def` `eq_or_ne` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `zero_sub` `MulZeroClass.zero_mul` `div_zero` `analyticAt_const` `AnalyticAt.fun_div` `AnalyticAt.fun_sub` `AnalyticAt.fun_mul` `analyticAt_id` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Mathlib.Meta.Positivity.ofReal_ne_zero_of_ne_zero`
`canonicalFactor_apply` 📖	mathematical	—	`canonicalFactor` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `ofReal` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	—
`canonicalFactor_apply_self` 📖	mathematical	—	`canonicalFactor` `Complex` `instZero`	—	`sub_self` `MulZeroClass.mul_zero` `div_zero`
`canonicalFactor_def` 📖	mathematical	—	`canonicalFactor` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `ofReal` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	—
`canonicalFactor_ne_zero` 📖	—	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Metric.closedBall`	—	—	`lt_imp_lt_of_le_of_le` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_zero_right` `norm_nonneg` `le_refl` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_mul` `RCLike.norm_conj` `sq` `norm_real` `abs_mul_abs_self` `canonicalFactor_apply` `div_ne_zero` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ne_of_gt` `Mathlib.Meta.Positivity.ofReal_pos`
`meromorphicNFOn_canonicalFactor` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero`	`MeromorphicNFOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `canonicalFactor` `Set.univ`	—	`eq_or_ne` `meromorphicNFAt_iff_analyticAt_or` `meromorphicOn_canonicalFactor` `Set.mem_univ` `meromorphicOrderAt_canonicalFactor` `WithTop.coe_lt_zero` `canonicalFactor_apply_self` `AnalyticAt.meromorphicNFAt` `analyticOnNhd_canonicalFactor`
`meromorphicOn_canonicalFactor` 📖	mathematical	—	`MeromorphicOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `canonicalFactor` `Set.univ`	—	`MeromorphicAt.fun_div` `MeromorphicAt.fun_sub` `MeromorphicAt.const` `MeromorphicAt.fun_mul` `MeromorphicAt.id`
`meromorphicOrderAt_canonicalFactor` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero`	`meromorphicOrderAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `instDenselyNormedField` `instNormedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `canonicalFactor` `WithTop` `WithTop.LinearOrderedAddCommGroup.instNeg` `Int.instAddCommGroup` `WithTop.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	—	`fun_meromorphicOrderAt_div` `MeromorphicAt.fun_sub` `MeromorphicAt.const` `MeromorphicAt.fun_mul` `MeromorphicAt.id` `fun_meromorphicOrderAt_mul` `MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff` `AnalyticAt.meromorphicNFAt` `AnalyticAt.fun_sub` `analyticAt_const` `AnalyticAt.fun_mul` `analyticAt_id` `normSq_eq_conj_mul_self` `normSq_eq_norm_sq` `sub_ne_zero` `ofReal_pow` `sq_eq_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `LT.lt.le` `Metric.pos_of_mem_ball` `norm_nonneg` `sub_zero` `mem_ball_iff_norm` `Int.instIsOrderedAddMonoid` `meromorphicOrderAt_const` `LT.lt.ne'` `meromorphicOrderAt_id_sub_const` `zero_add` `zero_sub`
`norm_canonicalFactor_eval_circle_eq_one` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Metric.sphere`	`Norm.norm` `Complex` `instNorm` `canonicalFactor` `Real` `Real.instOne`	—	`canonicalFactor.eq_1` `norm_div` `div_eq_iff` `norm_eq_zero` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ne_of_gt` `Mathlib.Meta.Positivity.ofReal_pos` `one_mul` `ofReal_pow` `normSq_eq_norm_sq` `normSq_eq_conj_mul_self` `sub_mul` `mul_comm` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `instCharZero` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass` `norm_mul` `RCLike.norm_conj` `norm_real` `norm_norm` `sub_zero`

---

← Back to Index