Mathlib Map

Theorems · Theorem · functional analysis

Real.norm_eq_abs

∀ (r : ℝ), ‖r‖ = |r|
Defined in
Mathlib.Analysis.Normed.Group.Real
Cited by
88 results in Mathlib
Foundations
Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.integral_eq_lintegral_of_nonneg_ae · cited by 31MeasureTheory.integral_eq…closure_ball · cited by 20closure_ballComplex.norm_intCast · cited by 12Complex.norm_intCastinterior_closedBall · cited by 8interior_closedBallNumberField.InfinitePlace.prod_eq_abs_norm · cited by 8InfinitePlace.prod_eq_abs…norm_smul_of_nonneg · cited by 7norm_smul_of_nonnegabs_real_inner_le_norm · cited by 7abs_real_inner_le_normInnerProductGeometry.angle_smul_right_of_pos · cited by 6InnerProductGeometry.angl…MeasureTheory.addHaar_image_le_mul_of_det_lt · cited by 4MeasureTheory.addHaar_ima…HasFDerivAt.hasFDerivAt_norm_smul · cited by 4HasFDerivAt.hasFDerivAt_n…MeasureTheory.memLp_norm_rpow_iff · cited by 4MeasureTheory.memLp_norm_…Orientation.oangle_add_right_smul_rotation_pi_div_two · cited by 4Orientation.oangle_add_ri…TFAE_exists_lt_isLittleO_pow · cited by 4TFAE_exists_lt_isLittleO_…Filter.Tendsto.integral_sub_linear_isLittleO_ae · cited by 3Tendsto.integral_sub_line…MeasureTheory.SimpleFunc.memLp_approxOn · cited by 3SimpleFunc.memLp_approxOnReal · cited by 25697RealNorm.norm · cited by 5413Norm.normabs · cited by 1814absReal.norm_eq_absCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement and proof · cited by 25,697
  • Norm.normstatement · cited by 5,413
  • absstatement · cited by 1,814

Cited by88

Results whose statement or proof uses this declaration.