Theorems · Theorem · real analysis
ENNReal.inv_pow
∀ {a : ENNReal} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n- Defined in
- Mathlib.Data.ENNReal.Inv
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topproof · cited by 9,680
- NNRealproof · cited by 4,310
- eq_or_neproof · cited by 1,117
- pow_zeroproof · cited by 1,094
- zero_powproof · cited by 361
- inv_oneproof · cited by 301
- pow_ne_zeroproof · cited by 208
- inv_powproof · cited by 140
- ENNReal.inv_zeroproof · cited by 37
- ENNReal.inv_topproof · cited by 36
- ENNReal.top_powproof · cited by 3
Cited by9
Results whose statement or proof uses this declaration.
- MeasureTheory.TendstoInMeasure.exists_seq_tendsto_aeproof · cited by 5
- BoxIntegral.unitPartition.volume_boxproof · cited by 2
- NumberField.mixedEmbedding.fundamentalCone.volume_normLeOneproof · cited by 2
- ENNReal.exists_inv_two_pow_ltproof · cited by 2
- ENNReal.inv_zpowproof · cited by 2
- ENNReal.tsum_two_zpow_neg_add_oneproof · cited by 1
- edist_le_of_edist_le_geometric_two_of_tendstoproof · cited by 1
- ProbabilityTheory.meas_ge_le_evariance_div_sqproof · cited by 1
- cauchySeq_of_edist_le_geometric_twoproof · cited by 0