Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 23:04 16a9031a

View on Github →

refactor(data/complex/*): replace complex.conj and is_R_or_C.conj with star (#9640) This PR replaces complex.conj and is_R_or_C.conj by the star operation defined in algebra/star. Both of these are replaced with star_ring_aut, which is also made available under the notation conj defined in the locale complex_conjugate. This effectively also upgrades conj from a ring_hom to a ring_aut. Fixes #9421

Estimated changes

added theorem star_ring_aut_apply
modified theorem complex.conj_cle_apply
modified theorem complex.continuous_conj
deleted theorem is_R_or_C.conj_to_complex
modified theorem coe_inv_circle_eq_conj
modified theorem fourier_neg
modified theorem real_inner_comm
deleted def complex.conj
deleted theorem complex.conj_bijective
deleted theorem complex.conj_conj
deleted theorem complex.conj_eq_zero
deleted theorem complex.conj_inj
deleted theorem complex.conj_involutive
modified theorem complex.conj_of_real
deleted theorem complex.conj_one
deleted theorem complex.conj_sub
deleted theorem is_R_or_C.conj_bijective
deleted theorem is_R_or_C.conj_conj
deleted theorem is_R_or_C.conj_div
deleted theorem is_R_or_C.conj_eq_zero
deleted theorem is_R_or_C.conj_inj
deleted theorem is_R_or_C.conj_inv
deleted theorem is_R_or_C.conj_involutive
modified theorem is_R_or_C.conj_to_real
modified theorem integral_conj