Theorems · Theorem · complex analysis
Complex.exp_zero
Complex.exp 0 = 1
- Defined in
- Mathlib.Analysis.Complex.Exponential
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Norm.normproof · cited by 5,413
- Finset.sumproof · cited by 5,195
- add_zeroproof · cited by 2,707
- Nat.cast_oneproof · cited by 2,501
- zero_addproof · cited by 2,366
- Finset.sum_congrproof · cited by 2,323
- MulZeroClass.mul_zeroproof · cited by 2,091
- Finset.rangeproof · cited by 1,341
- pow_zeroproof · cited by 1,094
- sub_selfproof · cited by 996
Cited by43
Results whose statement or proof uses this declaration.
- Real.exp_zeroproof · cited by 81
- Complex.exp_ne_zeroproof · cited by 19
- Complex.cpow_zeroproof · cited by 18
- Complex.exp_negproof · cited by 15
- Complex.one_cpowproof · cited by 14
- Complex.cos_zeroproof · cited by 14
- Complex.sin_zeroproof · cited by 8
- Complex.exp_pi_mul_Iproof · cited by 7
- Circle.exp_zeroproof · cited by 5
- Complex.cosh_sq_sub_sinh_sqproof · cited by 4
- Complex.ofReal_cpow_of_nonposproof · cited by 4
- ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prodproof · cited by 4