Theorems · Theorem · complex analysis
Complex.norm_mul
∀ (z w : ℂ), ‖z * w‖ = ‖z‖ * ‖w‖
- Defined in
- Mathlib.Analysis.Complex.Norm
- Cited by
- 59 results in Mathlib
- Foundations
- Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Norm.normstatement and proof · cited by 5,413
- Real.sqrtproof · cited by 545
- Complex.normSqproof · cited by 103
- Real.sqrt_mulproof · cited by 32
- Complex.norm_defproof · cited by 18
- Complex.normSq_nonnegproof · cited by 14
- Complex.normSq_mulproof · cited by 2
Cited by59
Results whose statement or proof uses this declaration.
- Complex.norm_expproof · cited by 33
- norm_circleMap_zeroproof · cited by 21
- Complex.canonicalFactor_ne_zeroproof · cited by 6
- Complex.exp_boundproof · cited by 6
- Polynomial.mahlerMeasure_mulproof · cited by 5
- NumberField.mixedEmbedding.normAtPlace_smulproof · cited by 5
- CircleIntegrable.outproof · cited by 5
- Complex.angle_eq_abs_argproof · cited by 4
- PeriodPair.hasFPowerSeriesOnBall_weierstrassPExceptproof · cited by 3
- Complex.abs_im_lt_normproof · cited by 3
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- ValueDistribution.proximity_mul_top_leproof · cited by 2