Theorems · Theorem · real analysis
Complex.contDiff_sin
∀ {n : WithTop ℕ∞}, ContDiff ℂ n Complex.sin- Cited by
- 9 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
- ENatstatement and proof · cited by 4,985
- WithTopstatement and proof · cited by 3,754
- ContDiffstatement · cited by 352
- Complex.sinstatement · cited by 258
- contDiff_idproof · cited by 40
- contDiff_constproof · cited by 36
- ContDiff.subproof · cited by 11
- contDiff_negproof · cited by 8
- ContDiff.div_constproof · cited by 8
- ContDiff.mulproof · cited by 8
- ContDiff.cexpproof · cited by 6
Cited by9
Results whose statement or proof uses this declaration.
- Real.contDiff_sinproof · cited by 11
- Complex.analyticAt_sinproof · cited by 2
- Complex.contDiffAt_tanproof · cited by 1
- ContDiff.csinproof · cited by 0
- Complex.analyticOn_sinproof · cited by 0
- Complex.analyticWithinAt_sinproof · cited by 0
- ContDiffAt.csinproof · cited by 0
- ContDiffOn.csinproof · cited by 0
- ContDiffWithinAt.csinproof · cited by 0