Theorems · Theorem · complex analysis
Real.exp_add
∀ (x y : ℝ), Real.exp (x + y) = Real.exp x * Real.exp y
- Defined in
- Mathlib.Analysis.Complex.Exponential
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- MulZeroClass.mul_zeroproof · cited by 2,091
- Complex.ofRealproof · cited by 1,654
- sub_zeroproof · cited by 938
- Complex.reproof · cited by 882
- Real.expstatement · cited by 871
- Complex.expproof · cited by 612
- Complex.mul_reproof · cited by 115
- Complex.ofReal_addproof · cited by 94
- Complex.exp_addproof · cited by 55
- Complex.exp_ofReal_improof · cited by 3
Cited by39
Results whose statement or proof uses this declaration.
- Real.log_mulproof · cited by 52
- Real.rpow_addproof · cited by 41
- Real.mul_rpowproof · cited by 37
- Real.exp_strictMonoproof · cited by 17
- Real.exp_subproof · cited by 13
- Polynomial.mahlerMeasure_mulproof · cited by 5
- ProbabilityTheory.IndepFun.mgf_addproof · cited by 4
- Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_rootsproof · cited by 4
- PhragmenLindelof.horizontal_stripproof · cited by 3
- Real.tendsto_exp_div_pow_atTopproof · cited by 3
- NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply''proof · cited by 3
- ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le_exp_addproof · cited by 2