Theorems · Definition · complex analysis
Complex.conjCLE
ℂ ≃L[ℝ] ℂ
Continuous linear equiv version of the conj function, from ℂ to ℂ.
This is an abbreviation for conjCAE coerced to a continuous linear map.
- Defined in
- Mathlib.Analysis.Complex.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 166 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 · cited by 25,697
- RingHom.idstatement · cited by 18,349
- Complexstatement · cited by 5,565
- ContinuousLinearEquivstatement · cited by 743
- Complex.conjCAEproof · cited by 27
- ContinuousAlgEquiv.toContinuousLinearEquivproof · cited by 12
Cited by15
Results whose statement or proof uses this declaration.
- Complex.conjCLE_normstatement · cited by 2
- IsConformalMap.is_complex_or_conj_linearstatement and proof · cited by 1
- isConformalMap_complex_linear_conjstatement · cited by 1
- isConformalMap_iff_is_complex_or_conj_linearstatement and proof · cited by 1
- UpperHalfPlane.smulFDeriv_J_mulstatement and proof · cited by 1
- UpperHalfPlane.hasStrictFDerivAt_smulproof · cited by 0
- AnalyticAt.harmonicAt_conjproof · cited by 0
- Complex.differentiable_conjproof · cited by 0
- Complex.conjCLE_applystatement · cited by 0
- Complex.conjCLE_coe_toLinearMapstatement · cited by 0
- Complex.conjCLE_enormstatement and proof · cited by 0
- Complex.conjCLE_nnormstatement · cited by 0