Theorems · Theorem · real analysis
Real.rpow_def_of_neg
∀ {x : ℝ}, x < 0 → ∀ (y : ℝ), x ^ y = Real.exp (Real.log x * y) * Real.cos (y * Real.pi)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites36
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
- Complexproof · cited by 5,565
- Nat.cast_zeroproof · cited by 1,870
- Real.pistatement and proof · cited by 1,774
- mul_assocproof · cited by 1,667
- Complex.ofRealproof · cited by 1,654
- Real.logstatement and proof · cited by 939
- Complex.reproof · cited by 882
- Real.expstatement and proof · cited by 871
- Complex.Iproof · cited by 866
- Complex.expproof · cited by 612
- Complex.improof · cited by 591
Cited by7
Results whose statement or proof uses this declaration.
- Real.sqrt_eq_rpowproof · cited by 25
- Real.abs_rpow_le_abs_rpowproof · cited by 7
- intervalIntegral.intervalIntegrable_rpow'proof · cited by 6
- Real.contDiffAt_rpow_of_neproof · cited by 4
- Real.hasStrictFDerivAt_rpow_of_negproof · cited by 2
- Real.rpow_def_of_nonposproof · cited by 1
- Real.rpow_eq_nhds_of_negproof · cited by 1