partialOrder 📖 | CompOp | 52 mathmath: not_le_iff, DirichletCharacter.zetaMul_prime_pow_nonneg, ArithmeticFunction.LSeries_positive, PositiveLinearMap.preGNS_norm_def, DifferentiableOn.nonneg_of_iteratedDeriv_nonneg, ClosedSubmodule.inner_real_eq_re_inner, ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn, PositiveLinearMap.preGNS_inner_def, CStarAlgebra.instNonnegSpectrumClassComplexNonUnital, Mathlib.Meta.Positivity.ofReal_nonneg, Differentiable.nonneg_of_iteratedDeriv_nonneg, LSeries.term_nonneg, DirichletCharacter.zetaMul_nonneg, arg_eq_zero_iff_zero_le, sq_nonneg_iff, neg_iff, ClosedSubmodule.mem_symplComp_iff, nonpos_iff, inv_natCast_cpow_ofReal_pos, Mathlib.Meta.Positivity.ofReal_pos, zero_lt_real, riemannZeta_pos_of_one_lt, LSeries.iteratedDeriv_alternating, LSeries.term_pos, not_le_zero_iff, pos_iff, re_eq_neg_norm, zero_le_real, LSeries.positive, sq_nonpos_iff, compl_Iic_zero, not_lt_zero_iff, RCLike.to_complex_nonneg_iff, Differentiable.apply_le_of_iteratedDeriv_nonneg, real_le_real, nonneg_iff, real_lt_real, le_def, ArithmeticFunction.iteratedDeriv_LSeries_alternating, monotone_ofReal, CStarAlgebra.instNonnegSpectrumClassComplexUnital, re_eq_norm, neg_re_eq_norm, re_nonneg_iff_nonneg, mem_slitPlane_iff_not_le_zero, Differentiable.apply_le_of_iteratedDeriv_alternating, PositiveLinearMap.preGNS_norm_sq, orderClosedTopology, LSeries.positive_of_differentiable_of_eqOn, not_lt_iff, arg_eq_pi_iff_lt_zero, lt_def
|