conj (complex conjugation)

Stream: new members

[Dima Pasechnik]

I am digging through some oldish code, and see conj there, meaning complex conjugate of a complex number. And unknown identifier 'conj' error. Did it get renamed in the past 8 months?

[Kevin Buzzard]

Maybe you need complex.conj?

[Ruben Van de Velde]

localized "notation `conj` := star_ring_aut" in complex_conjugate

[Ruben Van de Velde]

So you can use the general star thing or open_locale complex_conjugate, I think

[Dima Pasechnik]

Ruben Van de Velde said:

localized "notation `conj` := star_ring_aut" in complex_conjugate

Thanks, so adding that localized ... allowed that lemma to be proven, thanks! What happened to the old conj ?
(I presume it was good place to add it somewhere just after the top include statements.)

[Eric Rodriguez]

it got refactored and unified with the general star_ring_aut