Linear Algebra Done Right, Section 1A

Stream: general

[Martin C. Martin]

I've made a first pass at translating Sheldon Axler's Linear Algebra Done Right, section 1A, into Lean. Please find it on github here.. All feedback welcome! Should I continue along these same lines with the rest of the book?

[Martin C. Martin]

One question is, should I do the exercises? On the one hand, publishing solutions to exercises undermines the use of the book in class. On the other hand, most students don't know Lean, and even those who do might have a hard time understanding the proof and translating it into traditional hand written math.

[Julian Berman]

There's another attempt at this FWIW at https://github.com/Vilin97/linear-algebra-done-right, I think by @Vasily Ilin with a few others contributing.

(Which isn't to say you shouldn't proceed as is!)

[Eric Wieser]

A quick skim is a nice confirmation to me that using fin n → α in mathlib instead of vector n α was a good choice in terms of making proofs short!

[Eric Wieser]

(of course the real argument for using fin n →α is that it's a special case of ι → α, and so most of the theory can be developed there instead)

[Yakov Pechersky]

(deleted)

[Eric Wieser]

-- Would like to make n implicit, how do we split on cases of an implicit
-- argument?
@[simp]
def neg : ∀ (n : ℕ) (v : vector F n), vector F n

You just write {n : N} instead and it should just work.

[Martin C. Martin]

Julian Berman said:

There's another attempt at this

Thanks! My main goal is to learn, secondary goal is to contribute something of value to the community. If there's something more valuable in the first two years of a standard undergrad math curriculum, I'm happy to contribute that instead. Something from 3rd year would be a stretch but I'm up for that too. Spivak's Calculus comes to mind. But without consensus, I'm happy to stick with LADR.

[Martin C. Martin]

Eric Wieser said:

A quick skim is a nice confirmation to me that using fin n → α in mathlib instead of vector n α was a good choice in terms of making proofs short!

Thanks! I am a little concerned that using recursion and induction for something as simple as a tuple will make Lean seem more complicated than need be, so maybe fin n → α would be a better, especially if we can e.g. define addition as λ i, v[i] + w[i].

[Martin C. Martin]

Eric Wieser said:

You just write {n : N} instead and it should just work.

Oh right, I don't know why I didn't think of that!

[Eric Wieser]

For actually executing code, your inductive approach is probably more efficient

[Martin C. Martin]

Eric Wieser said:

For actually executing code, your inductive approach is probably more efficient

Reminds me of a joke.

An engineer, a physicist and a mathematician are at a conference, staying at a hotel. In the middle of the night, a fire breaks out. The engineer wakes up, sees the fire, sees the fire extinguisher, puts the fire out with the fire extinguisher, and goes back to sleep.

A little while later, another fire breaks out. This time, the physicist wakes up. Sees the fire, sees the extinguisher, calculates the angle to use the minimum amount of water, puts out the fire and goes back to sleep.

Wouldn't you know it, a third fire breaks out. This time the mathematician wakes up. Sees the fire, sees the extinguisher, says "Ah, a solution exists!" and goes back to sleep.

[Giovanni Mascellani]

(I'd have something to say to the hotel safety manager, though...)

[Martin C. Martin]

Julian Berman said:

There's another attempt at this FWIW at https://github.com/Vilin97/linear-algebra-done-right, I think by Vasily Ilin with a few others contributing.

(Which isn't to say you shouldn't proceed as is!)

Just took a look, it seems they're only doing the exercises and not the main text, whereas I'm doing the opposite, only the main text and not the exercises. :)

[Martin C. Martin]

Eric Wieser said:

(of course the real argument for using fin n →α is that it's a special case of ι → α, and so most of the theory can be developed there instead)

Example 1.22 is F^∞, which can't be defined recursively, and the most reasonable way to do it as ℕ → F. So even in LADR it would be simpler to use fin n → F. :)