Theorems · Theorem · complex analysis
norm_circleMap_zero
∀ (R θ : ℝ), ‖circleMap 0 R θ‖ = |R|
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Realstatement and proof · cited by 25,697
- Complexstatement · cited by 5,565
- Norm.normstatement and proof · cited by 5,413
- mul_oneproof · cited by 3,885
- zero_addproof · cited by 2,366
- absstatement and proof · cited by 1,814
- Complex.ofRealproof · cited by 1,654
- Complex.Iproof · cited by 866
- Complex.expproof · cited by 612
- circleMapstatement · cited by 117
- Complex.norm_realproof · cited by 105
- Complex.norm_mulproof · cited by 59
Cited by21
Results whose statement or proof uses this declaration.
- circleMap_mem_sphere'proof · cited by 14
- MeromorphicOn.circleIntegrable_log_normproof · cited by 11
- CircleIntegrable.outproof · cited by 5
- Real.circleAverage_monoproof · cited by 3
- Real.ContinuousOn.circleAverageproof · cited by 2
- circleIntegrable_iffproof · cited by 2
- hasSum_two_pi_I_cauchyPowerSeries_integralproof · cited by 2
- circleAverage_log_norm_sub_const₁proof · cited by 1
- ValueDistribution.Cartan.integrable_integral_norm_cartanKernelproof · cited by 1
- hasDerivAt_circleAverage_herglotzRieszKernel_smulproof · cited by 1
- norm_cauchyPowerSeries_leproof · cited by 1
- circleIntegral.norm_integral_le_of_norm_le_const'proof · cited by 1