Mathlib Map

Theorems · Theorem · field theory

Complex.add_re

∀ (z w : ℂ), (z + w).re = z.re + w.re
Defined in
Mathlib.Data.Complex.Basic
Cited by
22 results in Mathlib
Foundations
Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Complex.Gamma_add_one · cited by 12Complex.Gamma_add_oneReal.rpow_def_of_neg · cited by 7Real.rpow_def_of_negComplex.reLm · cited by 6Complex.reLmReal.cosh_eq · cited by 5Real.cosh_eqintegral_cpow · cited by 5integral_cpowComplex.differentiable_one_div_Gamma · cited by 4Complex.differentiable_on…ModularGroup.re_T_zpow_smul · cited by 3ModularGroup.re_T_zpow_sm…Complex.reAddGroupHom · cited by 3Complex.reAddGroupHomProbabilityTheory.hasDerivAt_integral_pow_mul_exp · cited by 3ProbabilityTheory.hasDeri…convex_halfSpace_re_gt · cited by 2convex_halfSpace_re_gtnorm_jacobiTheta₂_term · cited by 2norm_jacobiTheta₂_termhasSum_mellin_pi_mul_sq' · cited by 2hasSum_mellin_pi_mul_sq'convex_halfSpace_re_lt · cited by 1convex_halfSpace_re_ltComplex.arg_one_add_mem_Ioo · cited by 1Complex.arg_one_add_mem_I…HurwitzZeta.hasSum_int_hurwitzZetaOdd · cited by 1HurwitzZeta.hasSum_int_hu…Real · cited by 25697RealComplex · cited by 5565ComplexComplex.re · cited by 882Complex.reComplex.add_reCITED BYCITES

Cites3

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 · cited by 882

Cited by24

Results whose statement or proof uses this declaration.