Theorems · Theorem · field theory
Complex.ext_iff
∀ {z w : ℂ}, z = w ↔ z.re = w.re ∧ z.im = w.im- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · 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
- Complex.extproof · cited by 28
Cited by20
Results whose statement or proof uses this declaration.
- Complex.ofReal_mulproof · cited by 180
- Complex.ofReal_negproof · cited by 130
- Complex.ofReal_addproof · cited by 94
- Complex.ofReal_subproof · cited by 63
- Complex.ofReal_invproof · cited by 62
- Complex.re_add_improof · cited by 41
- Complex.conj_ofRealproof · cited by 41
- Complex.conj_Iproof · cited by 36
- Complex.I_mul_Iproof · cited by 35
- Complex.mk_eq_add_mul_Iproof · cited by 5
- Complex.add_conjproof · cited by 3
- Circle.exp_injOn_of_forall_sub_mem_Iooproof · cited by 3