Theorems · Definition · complex analysis
Function.Periodic.invQParam
ℝ → ℂ → ℂ
One-sided inverse of qParam h.
- Defined in
- Mathlib.Analysis.Complex.Periodic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Real.piproof · cited by 1,774
- Complex.ofRealproof · cited by 1,654
- Complex.Iproof · cited by 866
- Complex.logproof · cited by 187
Cited by19
Results whose statement or proof uses this declaration.
- Function.Periodic.cuspFunctionproof · cited by 18
- Function.Periodic.cuspFunction_eq_of_nonzerostatement and proof · cited by 4
- Function.Periodic.eq_cuspFunctionproof · cited by 4
- Function.Periodic.invQParam_tendstostatement · cited by 3
- Function.Periodic.qParam_right_invstatement · cited by 3
- Function.Periodic.cuspFunction_zero_of_zero_at_infproof · cited by 3
- UpperHalfPlane.differentiableAt_cuspFunctionproof · cited by 2
- Function.Periodic.cuspFunction_addproof · cited by 2
- Function.Periodic.cuspFunction_smulproof · cited by 2
- Function.Periodic.im_invQParamstatement · cited by 2
- Function.Periodic.im_invQParam_pos_of_norm_lt_onestatement · cited by 2
- Function.Periodic.tendsto_nhds_zerostatement and proof · cited by 2