Theorems · Theorem · real analysis
Real.mul_rpow
∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → (x * y) ^ z = x ^ z * y ^ z- Cited by
- 37 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.
Cites12
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
- mul_oneproof · cited by 3,885
- Real.logproof · cited by 939
- Real.expproof · cited by 871
- mul_nonnegproof · cited by 397
- add_mulproof · cited by 363
- Real.rpow_zeroproof · cited by 69
- Real.log_mulproof · cited by 52
- LE.le.lt_of_ne'proof · cited by 41
- Real.exp_addproof · cited by 39
- Real.rpow_def_of_posproof · cited by 35
- Real.rpow_def_of_nonnegproof · cited by 6
Cited by37
Results whose statement or proof uses this declaration.
- NNReal.mul_rpowproof · cited by 13
- Real.div_rpowproof · cited by 10
- AkraBazziRecurrence.GrowsPolynomially.rpowproof · cited by 3
- Asymptotics.IsBigOWith.rpowproof · cited by 2
- ZLattice.exists_finsetSum_norm_rpow_le_tsumproof · cited by 2
- isBigO_norm_Icc_restrict_atTopproof · cited by 2
- LiouvilleWith.add_ratproof · cited by 2
- LiouvilleWith.mul_ratproof · cited by 2
- integral_rpow_mul_exp_neg_mul_rpowproof · cited by 2
- ProbabilityTheory.rpow_abs_le_mul_max_exp_of_posproof · cited by 2
- EisensteinSeries.summand_boundproof · cited by 2
- AkraBazziRecurrence.rpow_p_mul_one_add_smoothingFn_geproof · cited by 1