Theorems · Theorem · real analysis
Real.rpow_neg_eq_inv_rpow
∀ (x y : ℝ), x ^ (-y) = x⁻¹ ^ y
See also rpow_neg for a version with (x ^ y)⁻¹ in the RHS.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- Complexproof · cited by 5,565
- Real.piproof · cited by 1,774
- Complex.ofRealproof · cited by 1,654
- Complex.reproof · cited by 882
- starRingEndproof · cited by 671
- Complex.argproof · cited by 220
- Complex.ofReal_negproof · cited by 130
- map_inv₀proof · cited by 106
- Complex.normSqproof · cited by 103
- Complex.ofReal_invproof · cited by 62
Cited by6
Results whose statement or proof uses this declaration.
- Real.rpow_neg_oneproof · cited by 22
- Real.inv_rpowproof · cited by 14
- Function.hasTemperateGrowth_one_add_norm_sq_rpowproof · cited by 9
- qExpansion_coeff_isBigO_of_norm_isBigOproof · cited by 2
- tendsto_rpow_neg_nhdsGT_zeroproof · cited by 1
- Mathlib.Meta.NormNum.rpow_isRat_eq_inv_rpowproof · cited by 0