Theorems · Theorem · order theory
sq_pos_of_pos
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀],
0 < a → 0 < a ^ 2- Cited by
- 11 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.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- MonoidWithZerostatement and proof · cited by 456
- mul_posproof · cited by 374
- sqproof · cited by 280
- PosMulStrictMonostatement and proof · cited by 151
Cited by11
Results whose statement or proof uses this declaration.
- SimpleGraph.FarFromTriangleFree.nonposproof · cited by 2
- EuclideanGeometry.dist_lt_of_sbtw_of_inner_eq_zeroproof · cited by 1
- ZetaAsymptotics.term_oneproof · cited by 1
- StieltjesFunction.ae_hasDerivAtproof · cited by 1
- Pell.IsFundamental.mul_inv_x_lt_xproof · cited by 1
- sum_div_nat_floor_pow_sq_le_div_sqproof · cited by 1
- sum_div_pow_sq_le_div_sqproof · cited by 1
- Complex.norm_cderiv_leproof · cited by 1
- OrthogonalFamily.summable_iff_norm_sq_summableproof · cited by 1
- Real.lt_sq_of_sqrt_ltproof · cited by 0
- EuclideanGeometry.inner_vsub_center_vsub_posproof · cited by 0