# Zulip Chat Archive

## Stream: new members

### Topic: linear_algebra, matrices and vectors

#### Martin C. Martin (Mar 27 2023 at 21:27):

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 (Mar 27 2023 at 21:29):

The preferred spelling of a n-tuple in mathlib is `ι → R`

, where `n = fintype.card ι`

#### Eric Wieser (Mar 27 2023 at 21:30):

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 (Mar 27 2023 at 21:30):

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

#### Martin C. Martin (Mar 27 2023 at 21:36):

Ah interesting, thanks.

#### Martin C. Martin (Mar 27 2023 at 21:50):

For `{x y : ℝ}`

, the type of `(x, y, x)`

is `ℝ × ℝ × ℝ`

. Can this be expressed as a `v : fin n → ℝ`

?

#### Eric Wieser (Mar 27 2023 at 21:51):

Yes, as `![x, y, z]`

which has type `fin 3 → ℝ`

, which you can use after `import data.fin.vec_notation`

#### Eric Wieser (Mar 27 2023 at 21:51):

And matrices can be written as `!![a, b; c, d]`

with a similar import

#### Kevin Buzzard (Mar 27 2023 at 21:56):

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 (Mar 27 2023 at 22:01):

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

Last updated: Dec 20 2023 at 11:08 UTC