sqr vs sq vs pow_two

Stream: general

[Bryan Gin-ge Chen]

(editing)

[Bryan Gin-ge Chen]

Examples: docs#real.sqrt_sqr, docs#sq_sub_sq, docs#pow_two

[Bryan Gin-ge Chen]

This came up in #5933. I'm split between pow_two and sq. I think we already have a ton of lemmas named using pow_two and it fits the naming convention the best. On the other hand it's relatively long compared to sq and potentially trickier for new users to find.

[Yakov Pechersky]

It's just a special case of pow_bit0... :upside_down:

[Bryan Gin-ge Chen]

Looks like sq is barely edging out pow_two at the moment. Supposing we go with that, would it be better to add aliases to the existing pow_two lemmas or just rename them?

[Benjamin Davidson]

There's also square, as in docs#complex.cos_square.

[Ryan Lahfa]

(deleted)

[Mario Carneiro]

Aliases make sense to me, at least for the common theorems that people might have muscle memory for

[Mario Carneiro]

(Also because there seems to be a fairly large number of people who prefer this name anyway)

[Benjamin Davidson]

Sorry it took so long but I finally got around to doing this! #7368