Unscoped `sq`

Stream: mathlib4

[Artie Khovanov]

Why is the lemma sq (alias of pow_two) unscoped? I think this name hould be deprecated.

[Yury G. Kudryashov]

The alias was introduced by @Benjamin Davidson in !3#7368

[Yury G. Kudryashov]

CC: @Kim Morrison @Eric Wieser

[Ruben Van de Velde]

Why should it be deprecated?

[Yury G. Kudryashov]

I guess, @Artie Khovanov thinks that it's too generic to be in the root namespace. On the one hand, it has no conflicts in Mathlib (yet). OTOH, this may be inconvenient for downstream projects.

[Ruben Van de Velde]

I could see arguments along those lines, but think they should be made rather than implied :)

[Yury G. Kudryashov]

Note: right now, I'm too sleepy to decide what I think about it.

[Artie Khovanov]

I'm saying having "sq" be a lemma in the root namespace is bad! For instance I have an inductive class with constructor sq.

[Eric Wieser]

Why does a global sq clash with an inductive constructor?

[Eric Wieser]

(Note that I agree that sq is a weird thing to have in the root namespace; not least because it's just a bad lemma name)

[Edward van de Meent]

e.g. inside of the namespace List, you want cons to refer to List.cons rather than getting an error that it's ambiguous because _root_.cons also exists

[Alex Meiburg]

Would it be better to name it sq_eq_mul or similar? Scoping it? Removing it entirely?

[Artie Khovanov]

I would advocate for removing the alias. Whether we rename pow_two to sq_eq.* is a separate question imo.

[Eric Wieser]

We have a lot of sq aliases for other lemmas

[Eric Wieser]

I think renaming sq to sq_eq would be enough

[Eric Wieser]

It seems weird to me to have a lemma name that consists of only one token

[Eric Wieser]

Not least because with only one token you're fighting for names with definitions.

[Artie Khovanov]

That's fair, let's do that

[Violeta Hernández]

sq feels weird to me. We don't have an alias twice.

[Eric Wieser]

Allowing sq as a token lets us ever so slightly reduce the insanity of the name of Pythagoras' theorem