image_convexHull vs convexHull_image

Stream: mathlib4

[Michael Rothgang]

mathlib 's naming is inconsistent: it's docs#LinearMap.convexHull_image, but docs#AffineMap.image_convexHull. Is there any reason why these should be different? Which direction should be preferred?

[Michael Rothgang]

I've filed #11298, adapting the AffineMap lemma to the LinearMap version, but I'll be happy to change things the other way.

[Patrick Massot]

It’s not a naming issue. Both names are correct. The issue that those lemmas have different opinions about sides.

[Michael Rothgang]

Yes, I know!

[Michael Rothgang]

The question is, is there a good reason the lemmas have different sides? Or should one flip one of them to match the other?

[Patrick Massot]

And clearly this has to be fixed.

[Patrick Massot]

I’m sure this is an accident.

[Patrick Massot]

You can wait a bit to see whether someone has strong opinion but I guess picking one at random is fine.

[Yaël Dillies]

Yes, I have a strong opinion and in fact meant to fix it and forgot several months ago.

[Yaël Dillies]

It should be f '' convexHull _ _ = convexHull _ (f '' s), the same way we have docs#map_add

[Michael Rothgang]

Thank you for the input. I have now flipped both lemmas to match this convention.
The diff includes two lemmas, for which I'm wondering if they should be flipped as well.

[Yaël Dillies]

Might as well

[Michael Rothgang]

Sure, done.

[Yaël Dillies]

CI is not green. I will maintainer merge the PR when it is.

[Michael Rothgang]

CI is green now.