| Name | Category | Theorems |
|---|
LE 📖 | CompData | — |
cast 📖 | CompOp | 46 mathmath: HurwitzZeta.hasSum_int_hurwitzZetaOdd, Matrix.isTotallyUnimodular_iff, hasSum_mellin_pi_mul_sq', sign_mul_self, deriv_abs, coe_one, Matrix.isTotallyUnimodular_iff_fintype, QuadraticForm.equivalent_signType_weighted_sum_squared, coe_zero, HasStrictFDerivAt.abs, hasDerivWithinAt_abs, map_cast, EReal.abs_mul_sign, NormedSpace.normalize_smul, sign_mul_abs, coe_neg, HasFDerivAt.abs, HasFDerivWithinAt.abs, castHom_apply, Matrix.IsTotallyUnimodular.apply, abs_mul_sign, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, hasStrictDerivAt_abs, EReal.coe_coe_sign, coe_neg_one, map_cast', self_mul_sign, DivisibleHull.qsmul_def, intCast_cast, exists_signed_sum', signedDist_smul, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, fderiv_norm_smul, HasFDerivAt.hasFDerivAt_norm_smul, hasDerivAt_abs, QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared, Affine.Simplex.ExcenterExists.signedInfDist_excenter, EReal.sign_mul_inv_abs, EReal.sign_mul_abs, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, Int.sign_eq_sign, exists_signed_sum, coe_pow, coe_zpow, coe_mul, EReal.sign_mul_inv_abs'
|
fin3Equiv 📖 | CompOp | — |
instBoundedOrder 📖 | CompOp | — |
instCoeDep 📖 | CompOp | — |
instCommGroupWithZero 📖 | CompOp | 9 mathmath: signHom_apply, pow_even, castHom_apply, zpow_even, sign_pow, pow_odd, coe_pow, coe_zpow, zpow_odd
|
instDecidableLE 📖 | CompOp | — |
instHasDistribNeg 📖 | CompOp | — |
instLE 📖 | CompOp | 16 mathmath: neg_one_lt_iff, nonpos_iff_ne_one, Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi, sign_nonneg_iff, neg_one_le, nonpos_iff, Real.Angle.toReal_nonneg_iff_sign_nonneg, nonneg_iff_ne_neg_one, le_neg_one_iff, neg_le_neg_iff, sign_nonpos_iff, one_le_iff, nonneg_iff, Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi, le_one, lt_one_iff
|
instLinearOrder 📖 | CompOp | 90 mathmath: HurwitzZeta.hasSum_int_hurwitzZetaOdd, sign_intCast, hasSum_mellin_pi_mul_sq', neg_one_lt_iff, sign_mul_self, deriv_abs, Affine.Simplex.sign_excenterWeights_singleton_pos, signHom_apply, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, EReal.sign_eq_and_abs_eq_iff_eq, sign_nonneg_iff, Affine.Simplex.sign_touchpointWeights_empty, HasStrictFDerivAt.abs, hasDerivWithinAt_abs, EReal.abs_mul_sign, sign_zero, NormedSpace.normalize_smul, sign_mul_abs, sign_eq_of_affineCombination_mem_affineSpan_single_lineMap, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, sign_pos, neg_one_lt_one, HasFDerivAt.abs, HasFDerivWithinAt.abs, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, not_one_lt, EReal.sign_mul, EReal.sign_coe, Affine.Simplex.sign_excenterWeights_singleton_neg, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, eventually_nhdsWithin_sign_eq_of_deriv_neg, abs_mul_sign, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, hasStrictDerivAt_abs, Orientation.oangle_sign_smul_left, Orientation.oangle_sign_smul_add_smul_smul_add_smul, eventually_nhdsWithin_sign_eq_of_deriv_pos, sign_mul, EReal.sign_bot, self_mul_sign, sign_apply, DivisibleHull.qsmul_def, sign_one, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.ExcenterExists.sign_touchpointWeights, Affine.Simplex.sign_touchpointWeights_singleton_pos, Orientation.oangle_sign_smul_right, sign_neg, signedDist_smul, neg_lt_neg_iff, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, Affine.Simplex.sign_touchpointWeights_singleton_neg, EReal.sign_top, fderiv_norm_smul, HasFDerivAt.hasFDerivAt_norm_smul, Affine.Simplex.sign_signedInfDist_touchpoint_empty, sign_nonpos_iff, sign_pow, StrictMono.sign_comp, hasDerivAt_abs, Affine.Simplex.sign_excenterWeights_empty, not_lt_neg_one, sign_eq_zero_iff, EReal.le_iff_sign, continuousAt_sign_of_neg, continuousAt_sign_of_pos, pos_iff, Affine.Simplex.ExcenterExists.signedInfDist_excenter, Real.Angle.sign_toReal, sign_eq_sign_or_eq_neg, EReal.sign_mul_inv_abs, Affine.Simplex.sign_signedInfDist_incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, EReal.sign_mul_abs, Orientation.oangle_sign_smul_add_smul_right, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, Polynomial.signVariations_eq_eraseLead_add_ite, lt_one_iff, EReal.sign_neg, Int.sign_eq_sign, Orientation.oangle_sign_smul_add_smul_left, continuousAt_sign_of_ne_zero, Right.sign_neg, neg_iff, Left.sign_neg, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, EReal.sign_mul_inv_abs', sign_eq_neg_one_iff, sign_eq_one_iff
|
instMul 📖 | CompOp | 8 mathmath: EReal.sign_mul, Orientation.oangle_sign_smul_left, Orientation.oangle_sign_smul_add_smul_smul_add_smul, sign_mul, Orientation.oangle_sign_smul_right, Orientation.oangle_sign_smul_add_smul_right, Orientation.oangle_sign_smul_add_smul_left, coe_mul
|
instNeg 📖 | CompOp | 49 mathmath: EuclideanGeometry.oangle_swap₁₃_sign, neg_one_lt_iff, Real.Angle.sign_neg, neg_eq_zero_iff, neg_eq_neg_one, Real.Angle.sign_two_nsmul_eq_neg_sign_iff, neg_eq_self_iff, neg_one_le, neg_one_lt_one, coe_neg, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, nonpos_iff, Real.Angle.sign_sub_pi, Affine.Simplex.sign_excenterWeights_singleton_neg, Orientation.oangle_sign_neg_left, EuclideanGeometry.oangle_swap₁₂_sign, Orientation.oangle_sign_sub_right_eq_neg, Orientation.oangle_sign_smul_sub_left, coe_neg_one, trichotomy, EReal.sign_bot, Orientation.oangle_sign_sub_left_eq_neg, sign_apply, Real.Angle.sign_pi_add, Real.Angle.sign_two_zsmul_eq_neg_sign_iff, Real.Angle.toReal_neg_iff_sign_neg, sign_neg, le_neg_one_iff, EuclideanGeometry.oangle_swap₂₃_sign, neg_le_neg_iff, neg_lt_neg_iff, Affine.Simplex.sign_touchpointWeights_singleton_neg, self_eq_neg_iff, Real.Angle.sign_add_pi, not_lt_neg_one, Orientation.oangle_sign_neg_right, sign_eq_sign_or_eq_neg, AffineSubspace.SOppSide.oangle_sign_eq_neg, Polynomial.signVariations_eq_eraseLead_add_ite, EReal.sign_neg, Right.sign_neg, Orientation.oangle_sign_smul_sub_right, neg_iff, Left.sign_neg, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, univ_eq, sign_eq_neg_one_iff, Real.Angle.sign_coe_neg_pi_div_two, Real.Angle.sign_antiperiodic
|
instOne 📖 | CompOp | 40 mathmath: neg_one_lt_iff, coe_one, Affine.Simplex.sign_excenterWeights_singleton_pos, neg_eq_neg_one, Affine.Simplex.sign_touchpointWeights_empty, neg_one_le, sign_pos, neg_one_lt_one, pow_even, not_one_lt, nonpos_iff, Real.Angle.toReal_mem_Ioo_iff_sign_pos, Affine.Simplex.sign_excenterWeights_singleton_neg, zpow_even, coe_neg_one, trichotomy, EReal.sign_bot, sign_apply, sign_one, Affine.Simplex.sign_touchpointWeights_singleton_pos, Real.Angle.toReal_neg_iff_sign_neg, sign_neg, le_neg_one_iff, pos_eq_one, Affine.Simplex.sign_touchpointWeights_singleton_neg, EReal.sign_top, Affine.Simplex.sign_excenterWeights_empty, Real.Angle.sign_coe_pi_div_two, not_lt_neg_one, one_le_iff, nonneg_iff, pos_iff, Affine.Simplex.sign_signedInfDist_incenter, le_one, lt_one_iff, neg_iff, univ_eq, sign_eq_neg_one_iff, sign_eq_one_iff, Real.Angle.sign_coe_neg_pi_div_two
|
instZero 📖 | CompOp | 28 mathmath: neg_one_lt_iff, nonpos_iff_ne_one, Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi, neg_eq_zero_iff, EuclideanGeometry.oangle_sign_eq_zero_iff_collinear, sign_nonneg_iff, coe_zero, neg_eq_self_iff, Real.Angle.sign_eq_zero_iff, sign_zero, Real.Angle.sign_zero, Real.Angle.sign_coe_pi, nonpos_iff, Real.Angle.toReal_nonneg_iff_sign_nonneg, nonneg_iff_ne_neg_one, trichotomy, sign_apply, exists_signed_sum', zero_eq_zero, self_eq_neg_iff, sign_nonpos_iff, sign_eq_zero_iff, nonneg_iff, pos_iff, Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi, lt_one_iff, neg_iff, univ_eq
|
sign 📖 | CompOp | 82 mathmath: HurwitzZeta.hasSum_int_hurwitzZetaOdd, sign_intCast, hasSum_mellin_pi_mul_sq', sign_mul_self, deriv_abs, Affine.Simplex.sign_excenterWeights_singleton_pos, signHom_apply, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, EReal.sign_eq_and_abs_eq_iff_eq, sign_nonneg_iff, Affine.Simplex.sign_touchpointWeights_empty, HasStrictFDerivAt.abs, hasDerivWithinAt_abs, EReal.abs_mul_sign, sign_zero, NormedSpace.normalize_smul, sign_mul_abs, sign_eq_of_affineCombination_mem_affineSpan_single_lineMap, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, sign_pos, HasFDerivAt.abs, HasFDerivWithinAt.abs, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, EReal.sign_mul, EReal.sign_coe, Affine.Simplex.sign_excenterWeights_singleton_neg, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, eventually_nhdsWithin_sign_eq_of_deriv_neg, abs_mul_sign, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, hasStrictDerivAt_abs, Orientation.oangle_sign_smul_left, Orientation.oangle_sign_smul_add_smul_smul_add_smul, eventually_nhdsWithin_sign_eq_of_deriv_pos, sign_mul, EReal.sign_bot, self_mul_sign, sign_apply, DivisibleHull.qsmul_def, sign_one, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.ExcenterExists.sign_touchpointWeights, Affine.Simplex.sign_touchpointWeights_singleton_pos, Orientation.oangle_sign_smul_right, sign_neg, signedDist_smul, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, Affine.Simplex.sign_touchpointWeights_singleton_neg, EReal.sign_top, fderiv_norm_smul, HasFDerivAt.hasFDerivAt_norm_smul, Affine.Simplex.sign_signedInfDist_touchpoint_empty, sign_nonpos_iff, sign_pow, StrictMono.sign_comp, hasDerivAt_abs, Affine.Simplex.sign_excenterWeights_empty, sign_eq_zero_iff, EReal.le_iff_sign, continuousAt_sign_of_neg, continuousAt_sign_of_pos, Affine.Simplex.ExcenterExists.signedInfDist_excenter, Real.Angle.sign_toReal, sign_eq_sign_or_eq_neg, EReal.sign_mul_inv_abs, Affine.Simplex.sign_signedInfDist_incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, EReal.sign_mul_abs, Orientation.oangle_sign_smul_add_smul_right, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, Polynomial.signVariations_eq_eraseLead_add_ite, EReal.sign_neg, Int.sign_eq_sign, Orientation.oangle_sign_smul_add_smul_left, continuousAt_sign_of_ne_zero, Right.sign_neg, Left.sign_neg, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, EReal.sign_mul_inv_abs', sign_eq_neg_one_iff, sign_eq_one_iff
|