Zulip Chat Archive

Stream: new members

Topic: linear_algebra, matrices and vectors

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


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