star vs. conj

Stream: mathlib4

[Geoffrey Irving]

Is there a good reason that star and the Complex conj notation are distinct in Mathlib?

[Yaël Dillies]

IMO the situation here is terrible wrt discoverability and simp normal form, and I have been wanting to remove the conj notation entirely

[Yaël Dillies]

I haven't had time to actually do this refactor, but if you or anyone else wants to try, I am very willing to review

[Geoffrey Irving]

Just star does seem better, as long as it shows up in Mathlib searches for conj(ugate) for newcomers.

[Eric Wieser]

I argued for this at the inception of conj, but the counterargument was that docs#LinearMap takes a ring-hom

[Eric Wieser]

Perhaps the answer is to have a special version of LinearMap.map_smulₛₗ for when sigma is starRingEnd