Theorems · Theorem · real analysis
ENNReal.rpow_one
∀ (x : ENNReal), x ^ 1 = x
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 200 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 · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- Top.topproof · cited by 9,680
- NNRealproof · cited by 4,310
- ENNReal.ofNNRealproof · cited by 1,279
- zero_lt_oneproof · cited by 598
- zero_le_oneproof · cited by 316
- LE.le.not_gtproof · cited by 189
- ENNReal.recTopCoeproof · cited by 48
- NNReal.rpow_oneproof · cited by 38
Cited by56
Results whose statement or proof uses this declaration.
- MeasureTheory.eLpNorm_one_eq_lintegral_enormproof · cited by 16
- IsSelfAdjoint.spectralRadius_eq_nnnormproof · cited by 7
- ENNReal.le_rpow_inv_iffproof · cited by 6
- ENNReal.rpow_inv_le_iffproof · cited by 5
- ENNReal.rpow_inv_rpowproof · cited by 5
- MeasureTheory.L1.norm_defproof · cited by 4
- ProbabilityTheory.evariance_lt_topproof · cited by 3
- ENNReal.rpow_add_le_mul_rpow_add_rpowproof · cited by 3
- HolderOnWith.interpolateproof · cited by 3
- MeasureTheory.mul_meas_ge_le_pow_eLpNormproof · cited by 3
- MeasureTheory.eLpNorm'_constproof · cited by 3
- ProbabilityTheory.Kernel.eLpNorm_densityProcess_leproof · cited by 3