Theorems · Theorem · complex analysis
Complex.norm_of_nonneg
∀ {r : ℝ}, 0 ≤ r → ‖↑r‖ = r- Defined in
- Mathlib.Analysis.Complex.Norm
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Complexstatement · cited by 5,565
- Norm.normstatement · cited by 5,413
- Complex.ofRealstatement · cited by 1,654
- abs_of_nonnegproof · cited by 279
- Complex.norm_realproof · cited by 105
Cited by20
Results whose statement or proof uses this declaration.
- Complex.norm_cpow_eq_rpow_re_of_posproof · cited by 21
- Complex.ofReal_logproof · cited by 14
- Complex.norm_natCastproof · cited by 12
- NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpaceproof · cited by 6
- Complex.arg_mul_cos_add_sin_mul_Iproof · cited by 5
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- Complex.GammaIntegral_convergentproof · cited by 3
- PhragmenLindelof.right_half_plane_of_tendsto_zero_on_realproof · cited by 2
- summable_jacobiTheta₂'_term_iffproof · cited by 2
- Complex.norm_nnratCastproof · cited by 1
- norm_jacobiTheta₂'_term_leproof · cited by 1
- Complex.norm_one_add_mul_inv_leproof · cited by 1