Theorems · Theorem · complex analysis
Complex.norm_ofNat
∀ (n : ℕ) [inst : n.AtLeastTwo], ‖OfNat.ofNat n‖ = OfNat.ofNat n
- Defined in
- Mathlib.Analysis.Complex.Norm
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Nat.AtLeastTwo
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement · cited by 5,565
- Norm.normstatement · cited by 5,413
- Nat.AtLeastTwostatement and proof · cited by 405
- Complex.norm_natCastproof · cited by 12
Cited by19
Results whose statement or proof uses this declaration.
- Complex.norm_twoproof · cited by 4
- PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExceptproof · cited by 4
- summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexpproof · cited by 2
- VectorFourier.norm_fourierPowSMulRight_leproof · cited by 2
- VectorFourier.norm_iteratedFDeriv_fourierPowSMulRightproof · cited by 2
- Complex.cos_boundproof · cited by 1
- Complex.sin_boundproof · cited by 1
- CStarAlgebra.exists_sum_four_unitaryproof · cited by 1
- tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_supportproof · cited by 1
- hasDerivAt_circleAverage_herglotzRieszKernel_smulproof · cited by 1
- norm_cauchyPowerSeries_leproof · cited by 1
- PeriodPair.weierstrassP_boundproof · cited by 1