linear_algebra, matrices and vectors

Stream: new members

[Martin C. Martin]

Hi,

It seems the linear_algebra directory in mathlib is abstract, and doesn't talk about matrices as 2D arrays of scalars, even linear_algebra.matrix is that right?

data.matrix seems to be the "2D array of scalars", and doesn't have a separate concept of vector, instead using 1xn or nx1 matrices as vectors. Is that also right?

Is there a structure like an n-tuple or n-dimensional vector that's compatible with linear_algebra?

The context is, I'm having a go at formalizing Axler's Linear Algebra Done Right, and in section 1.A he defined n-tuple, and I'm wondering where the equivalent definition is inside mathlib.

[Eric Wieser]

The preferred spelling of a n-tuple in mathlib is ι → R, where n = fintype.card ι

[Eric Wieser]

If you pushed really hard on the "no, I want to number each coefficient from 0 to n-1", then you can use fin n → R

[Eric Wieser]

Perhaps docs#matrix.mul_vec helps you see how this is expected to be used?

[Martin C. Martin]

Ah interesting, thanks.

[Martin C. Martin]

For {x y : ℝ}, the type of (x, y, x) is ℝ × ℝ × ℝ. Can this be expressed as a v : fin n → ℝ?

[Eric Wieser]

Yes, as ![x, y, z]which has type fin 3 → ℝ, which you can use after import data.fin.vec_notation

[Eric Wieser]

And matrices can be written as !![a, b; c, d] with a similar import

[Kevin Buzzard]

Note however that R x R x R is not definitionally equal to fin 3 -> R so it's a slight hassle converting from one to the other.

(Off-topic: I have a new phone and really should find that thread where Eric showed me how to type Unicode on android)

[Eric Wieser]

(I should really redo that with the last 2 years of vscode shortcut fixes...)