Order

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

Statistics

Metric	Count
Definitions `partialOrder`, `evalComplexOfReal`	2
Theorems `eq_re_of_ofReal_le`, `le_def`, `lt_def`, `monotone_ofReal`, `neg_iff`, `neg_re_eq_norm`, `nonneg_iff`, `nonpos_iff`, `not_le_iff`, `not_le_zero_iff`, `not_lt_iff`, `not_lt_zero_iff`, `pos_iff`, `re_eq_neg_norm`, `re_eq_norm`, `real_le_real`, `real_lt_real`, `sq_nonneg_iff`, `sq_nonpos_iff`, `zero_le_real`, `zero_lt_real`, `ofReal_ne_zero_of_ne_zero`, `ofReal_nonneg`, `ofReal_pos`	24
Total	26

Complex

Definitions

Name	Category	Theorems
`partialOrder` 📖	CompOp	38 math math: `not_le_iff`, `DirichletCharacter.zetaMul_prime_pow_nonneg`, `PositiveLinearMap.preGNS_norm_def`, `PositiveLinearMap.preGNS_inner_def`, `CStarAlgebra.instNonnegSpectrumClassComplexNonUnital`, `Mathlib.Meta.Positivity.ofReal_nonneg`, `DirichletCharacter.zetaMul_nonneg`, `arg_eq_zero_iff_zero_le`, `sq_nonneg_iff`, `neg_iff`, `nonpos_iff`, `inv_natCast_cpow_ofReal_pos`, `Mathlib.Meta.Positivity.ofReal_pos`, `zero_lt_real`, `riemannZeta_pos_of_one_lt`, `not_le_zero_iff`, `pos_iff`, `re_eq_neg_norm`, `zero_le_real`, `sq_nonpos_iff`, `compl_Iic_zero`, `not_lt_zero_iff`, `RCLike.to_complex_nonneg_iff`, `real_le_real`, `nonneg_iff`, `real_lt_real`, `le_def`, `monotone_ofReal`, `CStarAlgebra.instNonnegSpectrumClassComplexUnital`, `re_eq_norm`, `neg_re_eq_norm`, `re_nonneg_iff_nonneg`, `mem_slitPlane_iff_not_le_zero`, `PositiveLinearMap.preGNS_norm_sq`, `orderClosedTopology`, `not_lt_iff`, `arg_eq_pi_iff_lt_zero`, `lt_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_re_of_ofReal_le` 📖	mathematical	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `ofReal`	`re`	—	`conj_eq_iff_re` `conj_eq_iff_im` `le_def` `ofReal_im`
`le_def` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Real` `Real.instLE` `re` `im`	—	—
`lt_def` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Real` `Real.instLT` `re` `im`	—	—
`monotone_ofReal` 📖	mathematical	—	`Monotone` `Real` `Complex` `Real.instPreorder` `PartialOrder.toPreorder` `partialOrder` `ofReal`	—	—
`neg_iff` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `Real` `Real.instLT` `re` `Real.instZero` `im`	—	`lt_def`
`neg_re_eq_norm` 📖	mathematical	—	`Real` `Real.instNeg` `re` `Norm.norm` `Complex` `instNorm` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero`	—	`neg_re` `norm_neg` `re_eq_norm` `Iff.and` `neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `neg_eq_zero`
`nonneg_iff` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero` `Real` `Real.instLE` `Real.instZero` `re` `im`	—	`le_def`
`nonpos_iff` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero` `Real` `Real.instLE` `re` `Real.instZero` `im`	—	`le_def`
`not_le_iff` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Real` `Real.instLT` `re`	—	`le_def` `not_and_or` `not_le`
`not_le_zero_iff` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero` `Real` `Real.instLT` `Real.instZero` `re`	—	`not_le_iff`
`not_lt_iff` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Real` `Real.instLE` `re`	—	`lt_def` `not_and_or` `not_lt`
`not_lt_zero_iff` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `Real` `Real.instLE` `Real.instZero` `re`	—	`not_lt_iff`
`pos_iff` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `Real` `Real.instLT` `Real.instZero` `re` `im`	—	`lt_def`
`re_eq_neg_norm` 📖	mathematical	—	`re` `Real` `Real.instNeg` `Norm.norm` `Complex` `instNorm` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero`	—	`neg_eq_iff_eq_neg` `neg_re_eq_norm`
`re_eq_norm` 📖	mathematical	—	`re` `Norm.norm` `Complex` `instNorm` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero`	—	`norm_nonneg` `abs_re_eq_norm` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`real_le_real` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `ofReal` `Real` `Real.instLE`	—	—
`real_lt_real` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofReal` `Real` `Real.instLT`	—	—
`sq_nonneg_iff` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `im` `Real` `Real.instZero`	—	`nonneg_iff` `pow_two` `mul_re` `mul_im` `mul_comm` `Nat.instAtLeastTwoHAddOfNat` `mul_two` `mul_eq_zero_iff_right` `IsStrictOrderedRing.noZeroDivisors` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `two_ne_zero` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `mul_eq_zero` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `zero_pow` `Nat.instCharZero` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `sub_zero` `sq_nonneg`
`sq_nonpos_iff` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instZero` `re` `Real` `Real.instZero`	—	`nonpos_iff` `pow_two` `mul_re` `mul_im` `mul_comm` `Nat.instAtLeastTwoHAddOfNat` `mul_two` `mul_eq_zero_iff_right` `IsStrictOrderedRing.noZeroDivisors` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `two_ne_zero` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `mul_eq_zero` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `zero_add` `zero_pow` `Nat.instCharZero` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `zero_sub` `sq_nonneg`
`zero_le_real` 📖	mathematical	—	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero` `ofReal` `Real` `Real.instLE` `Real.instZero`	—	`real_le_real`
`zero_lt_real` 📖	mathematical	—	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `ofReal` `Real` `Real.instLT` `Real.instZero`	—	`real_lt_real`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalComplexOfReal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofReal_ne_zero_of_ne_zero` 📖	—	—	—	—	`Complex.ofReal_ne_zero`
`ofReal_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero` `Complex.ofReal`	—	`Complex.zero_le_real`
`ofReal_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Complex` `Preorder.toLT` `PartialOrder.toPreorder` `Complex.partialOrder` `Complex.instZero` `Complex.ofReal`	—	`Complex.zero_lt_real`

---

← Back to Index