naming convention: bundled versions of functions

Stream: mathlib4

[Yury G. Kudryashov]

We have different ways to name bundled versions of unbundled functions. E.g., docs#RCLike.reCLM docs#PiLp.projₗ docs#DFinsupp.filterLinearMap docs#zpowGroupHom docs#Pi.monoidHom docs#Pi.evalMulHom docs#LinearMap.pi docs#LinearMap.snd

[Yury G. Kudryashov]

Also, AFAIR sometimes prod is used for fun x => (f x, g x) and sometimes for Prod.map f g.

[Yury G. Kudryashov]

Should we choose a naming scheme here and apply it everywhere?

[Sébastien Gouëzel]

Yes, I think it would be very good to have a coherent naming scheme for all of these.

[Yury G. Kudryashov]

Let me revive this old topic. We have, e.g., docs#Pi.monoidHom and docs#LinearMap.pi. Which naming convention should we use?

[Yury G. Kudryashov]

In this case, I would go with MyHom.pi for 2 reasons:

• it looks more like a constructor for MyHom than some function bundled as MyHom; IMHO, the same applies to bundled versions of simple functions like Prod.fst, Prod.map, Pi.map;
• it enables the new-style dot notation.

P.S.: I've just found out that I'm responsible for the name pi.ring_hom introduced in !3#2133