Theorems · Theorem · order theory
abs_mul
∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (a b : α), |a * b| = |a| * |b|- Defined in
- Mathlib.Algebra.Order.Ring.Abs
- Cited by
- 98 results in Mathlib
- Foundations
- Depth 30 from the axioms, rests on 349 definitions · uses propext, Quot.sound
- Assumes
- RingLinearOrderIsOrderedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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 · cited by 1,814
- neg_negproof · cited by 960
- IsOrderedRingstatement and proof · cited by 777
- neg_mulproof · cited by 654
- mul_negproof · cited by 590
- mul_nonnegproof · cited by 397
- le_totalproof · cited by 294
- abs_of_nonnegproof · cited by 279
- abs_nonnegproof · cited by 168
- abs_of_nonposproof · cited by 53
Cited by99
Results whose statement or proof uses this declaration.
- Real.log_mulproof · cited by 52
- Real.abs_rpow_le_abs_rpowproof · cited by 7
- Affine.Simplex.ExcenterExists.dist_excenterproof · cited by 6
- AddCircle.norm_eqproof · cited by 6
- norm_jacobiTheta₂_term_leproof · cited by 5
- Polynomial.mahlerMeasure_mulproof · cited by 5
- absHomproof · cited by 5
- HasFDerivAt.hasFDerivAt_norm_smulproof · cited by 4
- abs_real_inner_div_norm_mul_norm_le_oneproof · cited by 4
- ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mulproof · cited by 3
- FormalMultilinearSeries.isLittleO_of_lt_radiusproof · cited by 3
- MeasureTheory.integral_comp_rpow_Ioiproof · cited by 3