type alias nightmare for AddAut.conj

Stream: mathlib4

[Antoine Chambert-Loir]

The definition of docs#AddAut.conj_symm_apply is

(AddEquiv.symm (conj g)) h = -g + h + g

but it seems to me that it misses one Additive.toMul, doesn't it?

This reflects in the definition of docs#AddAction.stabilizer_vadd_eq_stabilizer_map_conj
which also misses one.

[Eric Wieser]

Yes, this should be (Additive.toMul <| conj g).symm h = -g + h + g

[Antoine Chambert-Loir]

OK, I'll make a PR.

[Antoine Chambert-Loir]

#23978