feat(LinearAlgebra): add a variable_alias for VectorSpace

[Julian]

Taken directly from the variable_alias docs.

Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20.5Bvariable_alias.5D.20attribute.20is.20not.20used.20in.20Mathlib.3F

---

This is the first actual variable alias added to mathlib. I haven't reviewed variable_alias fully, but it seems like there's at least 3 ways they could be distributed in Mathlib:

• alongside whatever subfolder they "belong to" (which is what I've tentatively done here)
• In a file called Aliases somewhere near the thing they alias (which seems less discoverable to me)
• In a single file, a la Mathlib.TrainingWheels (with some less playful name) which is meant to define a bunch of more "friendly" aliases all in one place.

I kind of like the idea of the third thing as a future module but perhaps it can be synthesized if/when there are more aliases? For now as I say I've done the first one, but please let me know if someone prefers something else.

[github-actions]

PR summary dd812d8c50

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.VectorSpace	425

---

Declarations diff

+ VectorSpace

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Julian]

(I'm aware this is needed because I used Mathlib.Algebra.Module.Pi -- my rationale was that someone looking for the alias was likely to be newer, and that this other import seems reasonably cheap anyways. Let me know if that doesn't seem like a good enough reason to ignore this.)

[urkud]

Please add a test file with variable? [VectorSpace K V] and guard_msgs instead.

[PieterCuijpers]

(newbie:) Is there a standard format for adding a test file? What to name it, where to place it? Just asking so I can mimick the moves in my own PR.

[PieterCuijpers]

I just started to use an alias in my own PR on Quantales as well (branch#PieterCuijpers_Quantales / #17289) and basically follow the same route. I just defined the alias in the 'main file' where, I think, it belongs. The planned use, after all to me, is writing [VectorSpace a] is more natural (in a file that proofs something about vector spaces) than writing the unfolding of it.

In my case, my reviewers asked me to define a mixin IsQuantale instead of having a proper class Quantale.
The latter seems more natural to me from a 'software structure' point of view, but I understand that having the mixin leads to (much?) less overhead in re-proving theorems. The alias 'saves' me, so I can define at least the structure Quantale after all - which was the point of the whole file. Hence, I feel the alias belongs there.

But then again... this is my first PR ever... so I don't really now anything ;-)
Curious to learn what happens to your PR.

[Julian]

Aha! Thanks for the cross-link and info, I'll have a look at yours as well!

[urkud]

The docstring should underline the fact that this is not a class and it's here to be used with a variable? command, not as a [VectorSpace K V] assumption in a theorem.

[Julian]

(I agree with this) but it will apply to every use of variable_alias, correct? In which case it seems like perhaps variable_alias should automatically append that sort of message to the docstring of the declaration you use it on, presuming that should be possible, no?

[PieterCuijpers]

Aha! Thanks for the cross-link and info, I'll have a look at yours as well!

@Julian That would be great. However, I'm a bit weighing off two choices. I'd like the quantale PR to go through quickly, and having the variable_alias in there may slow down the reviewing process. It may be better to make it a separate PR after the first one got through. So I'll probably remove it for now and get back to you a.s.a.p. keeping an eye on this discussion for inspiration.

[PieterCuijpers]

The original PR for Quantale has been merged, now it's time to add the variable_alias. I've added a dependency to this PR, so that we can focus the discussion.