Mathlib Map

Theorems · Theorem · field theory

Complex.ext

∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
Defined in
Mathlib.Data.Complex.Basic
Cited by
28 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Complex.ext_iff · cited by 20Complex.ext_iffComplex.ofReal_log · cited by 14Complex.ofReal_logComplex.conj_eq_iff_im · cited by 9Complex.conj_eq_iff_imComplex.norm_mul_exp_arg_mul_I · cited by 6Complex.norm_mul_exp_arg_…Complex.sin_mul_I · cited by 5Complex.sin_mul_IComplex.normSq_eq_conj_mul_self · cited by 4Complex.normSq_eq_conj_mu…Complex.equivRealProd_symm_apply · cited by 4Complex.equivRealProd_sym…Complex.arg_neg_coe_angle · cited by 3Complex.arg_neg_coe_angleIsSelfAdjoint.mem_spectrum_eq_re · cited by 3IsSelfAdjoint.mem_spectru…Complex.normSq_eq_zero · cited by 3Complex.normSq_eq_zeroComplex.lim_eq_lim_im_add_lim_re · cited by 2Complex.lim_eq_lim_im_add…NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt · cited by 2IsPrimitiveRoot.nrRealPla…Complex.ofReal_mul' · cited by 2Complex.ofReal_mul'Complex.kahler · cited by 2Complex.kahlerPolynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv · cited by 2Gal.card_complex_roots_eq…Real · cited by 25697RealComplex · cited by 5565ComplexComplex.re · cited by 882Complex.reComplex.im · cited by 591Complex.imComplex.extCITED BYCITES

Cites4

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
  • Complex.restatement and proof · cited by 882
  • Complex.imstatement and proof · cited by 591

Cited by28

Results whose statement or proof uses this declaration.