Theorems · Theorem · real analysis
Complex.ofReal_cpow
∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), ↑(x ^ y) = ↑x ^ ↑y- Cited by
- 36 results in Mathlib
- Foundations
- Depth 194 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.
- Realstatement and proof · cited by 25,697
- Complexstatement · cited by 5,565
- Complex.ofRealstatement and proof · cited by 1,654
- Real.logproof · cited by 939
- Complex.expproof · cited by 612
- Complex.logproof · cited by 187
- Complex.ofReal_mulproof · cited by 180
- Complex.ofReal_expproof · cited by 44
- Complex.ofReal_logproof · cited by 14
- Real.rpow_def_of_nonnegproof · cited by 6
Cited by36
Results whose statement or proof uses this declaration.
- Real.rpow_mulproof · cited by 67
- ProbabilityTheory.complexMGF_id_gaussianRealproof · cited by 3
- Complex.inv_natCast_cpow_ofReal_posproof · cited by 3
- Real.integral_rpow_mul_exp_neg_mul_Ioiproof · cited by 3
- Complex.Gamma_one_half_eqproof · cited by 3
- Complex.cpow_mul_ofReal_nonnegproof · cited by 2
- Complex.cpow_ofRealproof · cited by 2
- integral_gaussian_complexproof · cited by 2
- Real.tendsto_one_add_rpow_exp_of_tendstoproof · cited by 2
- Complex.GammaIntegral_ofRealproof · cited by 2
- LSeries.tendsto_cpow_mul_atTopproof · cited by 2
- Complex.Gamma_mul_Gamma_add_halfproof · cited by 2