Mathlib Map

Theorems · Definition · field theory

Complex.equivRealProd

ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Defined in
Mathlib.Data.Complex.Basic
Cited by
15 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

polarCoord · cited by 25polarCoordComplex.equivRealProdAddHom · cited by 4Complex.equivRealProdAddH…Complex.equivRealProd_apply · cited by 4Complex.equivRealProd_app…Complex.equivRealProd_symm_apply · cited by 4Complex.equivRealProd_sym…Complex.preimage_equivRealProd_prod · cited by 3Complex.preimage_equivRea…Cardinal.mk_complex · cited by 2Cardinal.mk_complexComplex.antilipschitz_equivRealProd · cited by 2Complex.antilipschitz_equ…Complex.reProdIm_subset_iff · cited by 1Complex.reProdIm_subset_i…Complex.rectangle_eq_convexHull · cited by 1Complex.rectangle_eq_conv…Complex.lipschitz_equivRealProd · cited by 1Complex.lipschitz_equivRe…Complex.equivRealProd_apply_le · cited by 1Complex.equivRealProd_app…Complex.equivRealProd_apply_le' · cited by 1Complex.equivRealProd_app…NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply · cited by 0mixedEmbedding.mixedSpace…polarCoord_apply · cited by 0polarCoord_applyComplex.isUniformEmbedding_equivRealProd · cited by 0Complex.isUniformEmbeddin…Real · cited by 25697RealEquiv · cited by 8337EquivComplex · cited by 5565ComplexComplex.re · cited by 882Complex.reComplex.im · cited by 591Complex.imComplex.equivRealProdCITED BYCITES

Cites5

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
  • Equivstatement · cited by 8,337
  • Complexstatement and proof · cited by 5,565
  • Complex.reproof · cited by 882
  • Complex.improof · cited by 591

Cited by17

Results whose statement or proof uses this declaration.