Theorems · Theorem · order theory
mul_pos_of_neg_of_neg
∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
[AddRightStrictMono R] [AddRightReflectLT R] {a b : R}, a < 0 → b < 0 → 0 < a * b- Cited by
- 40 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- PartialOrderstatement and proof · cited by 6,410
- MulZeroClass.zero_mulproof · cited by 1,625
- ExistsAddOfLEstatement and proof · cited by 330
- AddRightStrictMonostatement and proof · cited by 160
- MulPosStrictMonostatement and proof · cited by 94
- AddRightReflectLTstatement and proof · cited by 29
- mul_lt_mul_of_neg_rightproof · cited by 6
Cited by40
Results whose statement or proof uses this declaration.
- mul_self_posproof · cited by 17
- mul_pos_iffproof · cited by 8
- summable_jacobiTheta₂_term_iffproof · cited by 4
- Real.cos_arcsinproof · cited by 4
- Real.binEntropy_neg_of_negproof · cited by 4
- Real.two_mul_arctanproof · cited by 3
- Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eqproof · cited by 3
- EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_radius_lt_distproof · cited by 2
- Real.self_sub_one_lt_mul_logproof · cited by 2
- pow_mem_ballproof · cited by 2
- Real.deriv_arcsin_auxproof · cited by 2
- Real.sin_arccosproof · cited by 2