Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-03 03:14 caa58cbf

View on Github →

chore(data/{complex,is_R_or_C}/basic): fix name of eq_conj_iff_* lemmas (#18922) These were all about conj x = x not x = conj x.

Estimated changes

Modified src/analysis/complex/upper_half_plane/metric.lean

Modified src/analysis/inner_product_space/positive.lean

Modified src/analysis/inner_product_space/spectrum.lean

Modified src/analysis/inner_product_space/symmetric.lean

Modified src/analysis/special_functions/gamma.lean

Modified src/data/complex/basic.lean

added theorem complex.conj_eq_iff_im

added theorem complex.conj_eq_iff_re

added theorem complex.conj_eq_iff_real

deleted theorem complex.eq_conj_iff_im

deleted theorem complex.eq_conj_iff_re

deleted theorem complex.eq_conj_iff_real

Modified src/data/complex/exponential.lean

Modified src/data/is_R_or_C/basic.lean

added theorem is_R_or_C.conj_eq_iff_re

added theorem is_R_or_C.conj_eq_iff_real

deleted theorem is_R_or_C.eq_conj_iff_re

deleted theorem is_R_or_C.eq_conj_iff_real

Modified src/field_theory/polynomial_galois_group.lean

Modified src/linear_algebra/matrix/hermitian.lean

Modified src/number_theory/number_field/embeddings.lean