Theorems · Theorem · complex analysis
Complex.cos_zero
Complex.cos 0 = 1
- Defined in
- Mathlib.Analysis.Complex.Trigonometric
- Cited by
- 14 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
- MulZeroClass.zero_mulproof · cited by 1,625
- Complex.Iproof · cited by 866
- Complex.expproof · cited by 612
- neg_zeroproof · cited by 542
- Complex.cosstatement · cited by 279
- Complex.exp_zeroproof · cited by 43
- add_self_div_twoproof · cited by 18
Cited by14
Results whose statement or proof uses this declaration.
- Real.cos_zeroproof · cited by 38
- Complex.cos_eq_one_iffproof · cited by 3
- Polynomial.Chebyshev.T_complex_cosproof · cited by 3
- Complex.arg_eq_zero_iffproof · cited by 3
- Complex.tendsto_euler_sin_prodproof · cited by 3
- Complex.tan_zeroproof · cited by 3
- EulerSine.sin_pi_mul_eqproof · cited by 1
- Complex.cos_int_mul_two_piproof · cited by 0
- Complex.cos_int_mul_two_pi_add_piproof · cited by 0
- Complex.cos_int_mul_two_pi_sub_piproof · cited by 0
- Complex.cos_nat_mul_two_piproof · cited by 0
- Complex.cos_nat_mul_two_pi_add_piproof · cited by 0