Theorems · Theorem · real analysis
NNReal.rpow_natCast
∀ (x : NNReal) (n : ℕ), x ^ ↑n = x ^ n
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound
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
- NNRealstatement and proof · cited by 4,310
- NNReal.toRealproof · cited by 1,260
- NNReal.eqproof · cited by 201
- Real.rpow_natCastproof · cited by 93
Cited by14
Results whose statement or proof uses this declaration.
- ENNReal.rpow_natCastproof · cited by 18
- NNReal.rpow_ofNatproof · cited by 4
- NNReal.rpow_intCastproof · cited by 4
- FormalMultilinearSeries.radius_eq_liminfproof · cited by 2
- ModP.mul_ne_zero_of_pow_p_ne_zeroproof · cited by 1
- NNReal.eventually_pow_one_div_leproof · cited by 1
- NumberField.mixedEmbedding.adjust_fproof · cited by 1
- NNReal.rpow_natCast_mulproof · cited by 1
- Mathlib.Meta.NormNum.IsNat.nnreal_rpow_eq_nnreal_powproof · cited by 0
- MeasureTheory.euclideanHausdorffMeasure_homothety_imageproof · cited by 0
- MeasureTheory.euclideanHausdorffMeasure_homothety_preimageproof · cited by 0
- CFC.rpow_natCastproof · cited by 0