Theorems · Theorem · order theory
sq_abs
∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a : α), |a| ^ 2 = a ^ 2- Defined in
- Mathlib.Algebra.Order.Ring.Abs
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
- Assumes
- RingLinearOrder
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.
- LinearOrderstatement and proof · cited by 8,572
- Ringstatement and proof · cited by 7,463
- absstatement and proof · cited by 1,814
- sqproof · cited by 280
- abs_mul_abs_selfproof · cited by 21
Cited by49
Results whose statement or proof uses this declaration.
- sq_le_sqproof · cited by 16
- sq_lt_sqproof · cited by 12
- ProbabilityTheory.variance_eq_integralproof · cited by 10
- MeasureTheory.MemLp.integrable_sqproof · cited by 5
- MeasureTheory.memLp_two_iff_integrable_sqproof · cited by 3
- integrable_inv_one_add_sqproof · cited by 3
- hasSum_mellin_pi_mul_sqproof · cited by 3
- EuclideanSpace.volume_ballproof · cited by 2
- Nat.sq_add_sq_zmodEqproof · cited by 2
- OrthonormalBasis.sum_sq_inner_rightproof · cited by 2
- CStarModule.norm_inner_leproof · cited by 2
- Complex.abs_re_lt_normproof · cited by 2