Theorems · Theorem · complex analysis
sineTerm_ne_zero
∀ {x : ℂ}, x ∈ Complex.integerComplement → ∀ (n : ℕ), 1 + sineTerm x n ≠ 0- Cited by
- 1 results in Mathlib
- Foundations
- Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Complexstatement and proof · cited by 5,565
- one_mulproof · cited by 2,841
- neg_negproof · cited by 960
- CharZeroproof · cited by 932
- Int.cast_natCastproof · cited by 393
- Int.cast_oneproof · cited by 371
- AddMonoidWithOneproof · cited by 313
- Int.cast_addproof · cited by 124
- add_eq_zero_iff_eq_negproof · cited by 49
- eq_div_iffproof · cited by 38
- Complex.integerComplementstatement and proof · cited by 30
Cited by1
Results whose statement or proof uses this declaration.
- logDeriv_prod_sineTerm_eq_sum_cotTermproof · cited by 1