Theorems · Theorem · complex analysis
Real.exp_zero
Real.exp 0 = 1
- Defined in
- Mathlib.Analysis.Complex.Exponential
- Cited by
- 81 results in Mathlib
- Foundations
- Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complex.reproof · cited by 882
- Real.expstatement · cited by 871
- Complex.exp_zeroproof · cited by 43
Cited by81
Results whose statement or proof uses this declaration.
- Real.log_oneproof · cited by 91
- Complex.norm_cpow_eq_rpow_re_of_posproof · cited by 21
- Real.add_one_le_expproof · cited by 13
- ProbabilityTheory.mgf_zero'proof · cited by 7
- Real.exp_lt_one_iffproof · cited by 7
- ProbabilityTheory.integral_id_gaussianRealproof · cited by 6
- Real.exp_le_one_iffproof · cited by 6
- Real.geom_mean_le_arith_mean_weightedproof · cited by 5
- EReal.exp_zeroproof · cited by 5
- Complex.norm_cpow_eq_rpow_re_of_nonnegproof · cited by 4
- Complex.norm_cpow_of_impproof · cited by 4
- summable_jacobiTheta₂_term_iffproof · cited by 4