Should docs#Complex.conj_ofReal be `@[simp]`?

Stream: mathlib4

[Anne Baanen]

This came up in #14601: since docs#RCLike.conj_ofReal is @[simp] and all the other Complex.conj lemmas are @[simp], shouldn't docs#Complex.conj_ofReal as well?

[Anne Baanen]

Adding the @[simp] tag didn't cause any linting issues in the file itself, let's see if the same holds when I build the entire library...

[Anne Baanen]

The build passes, so here's a PR: #14648