Mathlib Map

Theorems · Theorem · field theory

Complex.neg_re

∀ (z : ℂ), (-z).re = -z.re
Defined in
Mathlib.Data.Complex.Basic
Cited by
16 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.

integral_cexp_quadratic · cited by 5integral_cexp_quadraticsummable_riemannZetaSummand · cited by 4summable_riemannZetaSumma…norm_cexp_neg_mul_sq · cited by 4norm_cexp_neg_mul_sqComplex.tsum_exp_neg_quadratic · cited by 3Complex.tsum_exp_neg_quad…Complex.norm_prime_cpow_le_one_half · cited by 2Complex.norm_prime_cpow_l…GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I · cited by 2GaussianFourier.norm_cexp…Complex.neg_re_eq_norm · cited by 1Complex.neg_re_eq_normDirichletCharacter.eulerProduct_log_eq_LSeries · cited by 1DirichletCharacter.eulerP…Complex.re_neg_ne_zero_of_re_pos · cited by 1Complex.re_neg_ne_zero_of…Complex.continuousAt_arg_coe_angle · cited by 1Complex.continuousAt_arg_…Complex.continuousAt_ofReal_cpow · cited by 1Complex.continuousAt_ofRe…Polynomial.cyclotomic_eval_lt_add_one_pow_totient · cited by 1Polynomial.cyclotomic_eva…integral_exp_mul_Ioi · cited by 1integral_exp_mul_IoifourierIntegral_gaussian · cited by 0fourierIntegral_gaussianintegral_Ioi_cpow_of_lt · cited by 0integral_Ioi_cpow_of_ltReal · cited by 25697RealComplex · cited by 5565ComplexComplex.re · cited by 882Complex.reComplex.neg_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 by16

Results whose statement or proof uses this declaration.