Theorems · Theorem · field theory
Complex.inv_im
∀ (z : ℂ), z⁻¹.im = -z.im / Complex.normSq z
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- zero_addproof · cited by 2,366
- MulZeroClass.mul_zeroproof · cited by 2,091
- Complex.reproof · cited by 882
- MonoidWithZeroHomstatement · cited by 704
- starRingEndproof · cited by 671
- neg_mulproof · cited by 654
- Complex.imstatement and proof · cited by 591
- Complex.mul_improof · cited by 107
- Complex.normSqstatement and proof · cited by 103
Cited by13
Results whose statement or proof uses this declaration.
- Complex.ofReal_invproof · cited by 62
- UpperHalfPlane.im_inv_neg_coe_posproof · cited by 7
- Complex.div_improof · cited by 4
- Complex.angle_eq_abs_argproof · cited by 4
- Complex.div_reproof · cited by 4
- jacobiTheta₂_functional_equationproof · cited by 3
- ProbabilityTheory.complexMGF_id_gaussianRealproof · cited by 3
- qExpansion_coeff_isBigO_of_norm_isBigOproof · cited by 2
- GaussianInt.toComplex_re_divproof · cited by 1
- GaussianInt.normSq_div_sub_div_lt_oneproof · cited by 1
- jacobiTheta₂'_functional_equationproof · cited by 1
- GaussianInt.toComplex_im_divproof · cited by 1