## Stream: general

### Topic: sylvester's law of inertia

#### Johan Commelin (May 22 2020 at 08:10):

If there are people looking for an interesting first project to work on, with the aim of making a PR to mathlib, I'm willing to coach #2551 on Sylvester's law of inertia

#### Sam Lichtenstein (May 23 2020 at 03:30):

I was looking at that PR and when trying to figure out what ingredients are already in mathlib, I realized that I don't really know how experts navigate the library. Do you typically grep the source tree directly? Use the google search on the mathlib docs webpage? Some better method I don't know about (maybe a VSCode or emacs trick)? Relatedly, google search for "eigenvector" turned up no hits in the mathlib docs, and the same when searching the github repo (which I guess would also turn up PRs that mentioned this term, if there were any?) -- this seemed surprising to me. So I grepped and found only the following [using a terminal with poor unicode support]

\$ grep -r eigenv .
./archive/sensitivity.lean:lemma exists_eigenvalue (H : set (Q (m + 1))) (hH : Card H ΓëÑ 2^m + 1) :
./archive/sensitivity.lean:  rcases exists_eigenvalue H hH with Γƒ¿y, Γƒ¿Γƒ¿y_mem_H, y_mem_gΓƒ⌐, y_neΓƒ⌐Γƒ⌐,


Am I somehow missing a bunch of linear algebra stuff, or is the current state of the art quite barebones?

#### Mario Carneiro (May 23 2020 at 03:37):

Eigenvalues are not developed. I think this was blocked on the characteristic polynomial, but that might be solved now

#### Mario Carneiro (May 23 2020 at 03:38):

I suppose that the eigenvalues of a linear map are relatively easy to define

#### Mario Carneiro (May 23 2020 at 03:39):

although maybe it is more complicated if you want the eigenvalues to live in an algebraic extension of the scalar ring of the module

#### Sam Lichtenstein (May 23 2020 at 03:42):

" I think this was blocked on the characteristic polynomial, but that might be solved now"

Does this imply that there is a bunch of quasi-written code out there in various people's clones? In general, is there a way to distinguish cases where (supposedly simple thing X) is missing from mathlib because nobody has bothered to formalize it, from other cases where it is missing because there is some key technical bottleneck or disagreement about the implementation, and once that's resolved X is already effectively done?

#### Mario Carneiro (May 23 2020 at 03:45):

the best way is to ask here

#### Mario Carneiro (May 23 2020 at 03:47):

if you are lucky there might be an issue about it, or it could be on a docs or project page, but I would say that is the minority

#### Sam Lichtenstein (May 23 2020 at 03:47):

I guess that is a good pragmatic answer but doesn't seem like an ideal, scalable solution? I see now that the "undergraduate math list" thread in #general started with some complaints related to mine above, about navigability / discoverability

#### Sam Lichtenstein (May 23 2020 at 03:49):

also, to clarify, am I correct that the community's convention is NOT to allow sorry in committed .lean files in mathlib, nor to clutter these files with comments containing long TODO lists of lemmas/theorems that would be nice to have eventually? so github issues are the "canonical" place to look for known missing features (aside from asking here)

#### Bryan Gin-ge Chen (May 23 2020 at 03:50):

sorry is definitely not allowed, except possibly in the roadmap/ directory where there's some trick for using it.

#### Sam Lichtenstein (May 23 2020 at 03:52):

ah, I had not noticed the roadmap/ directory, which is a nice idea -- but seems sparsely populated :)

#### Bryan Gin-ge Chen (May 23 2020 at 03:52):

I don't know what to say about long TODOs. I guess I don't see why anyone would want to add very long TODOs.

GitHub issues is the right place to look outside of Zulip for now. We should make an effort to document more things there, since Zulip is definitely less accessible.

#### Sam Lichtenstein (May 23 2020 at 03:53):

I guess with only 80 open issues, all of mathematics is close to being complete :-)

#### Bryan Gin-ge Chen (May 23 2020 at 03:53):

Lots of things we do now aren't scalable. I think we can worry about optimizing our processes when we have more contributors and contributions.

#### Mario Carneiro (May 23 2020 at 03:54):

Sam Lichtenstein said:

I guess that is a good pragmatic answer but doesn't seem like an ideal, scalable solution? I see now that the "undergraduate math list" thread in #general started with some complaints related to mine above, about navigability / discoverability

Does this scale? Probably not, but that doesn't mean it's not the appropriate solution at this scale. Mathlib procedures have changed as we have grown, and they will continue to change

#### Sam Lichtenstein (May 23 2020 at 03:54):

yeah that makes sense -- I'm just trying to figure out how to understand the lay of the land as a newbie

#### Mario Carneiro (May 23 2020 at 03:55):

Anyway, here's something to get you started on eigenvectors:

import linear_algebra.basic

variables {R : Type*} {M : Type*}
variables [comm_ring R] [add_comm_group M] [module R M]

def eigenvectors (f : M →ₗ[R] M) (Λ : R) : submodule R M :=
{ carrier := {v | f v = Λ • v},
zero := f.map_zero.trans (smul_zero _).symm,
add := λ a b ha hb, by simp [*, smul_add] at *,
smul := λ c a ha, by simp [*, smul_comm] at * }

@[simp] theorem mem_eigenvectors {f : M →ₗ[R] M} {Λ : R} {v} :
v ∈ eigenvectors f Λ ↔ f v = Λ • v := iff.rfl


thanks!

#### Mario Carneiro (May 23 2020 at 03:58):

def eigenvalues (f : M →ₗ[R] M) : set R := {Λ | eigenvectors f Λ ≠ ⊥}


#### Scott Morrison (May 23 2020 at 05:13):

Regarding TODO, roadmap/, and the issues page: I think we'd be very happy with contributions in any of these three directions (as long as they are specific enough to be useful: a list of aspirations is only helpful if you're planning on working on them soon). I think for now everyone is open minded about which system works best, and if one of those three gains significant momentum then we can formalise that as the preferred approach.

#### Yury G. Kudryashov (May 23 2020 at 05:31):

roadmap/ works like an issue + branch with some preliminary work.

#### Scott Morrison (May 23 2020 at 05:35):

I would love to see more roadmaps. I think it's much more accessible to get started on something if someone with more mathlib design experience has already made a guess about how the primary definitions should be structured, and indicated which lemmas to aim for.

#### Kevin Buzzard (May 23 2020 at 07:13):

I wanted some basic number theory and algebra done at some point, and wanted to flag that it was not done, and so I just made a project. Nobody is working hard on it but if it's still in that state in July I'll see if I can get some students working on it

#### Patrick Massot (May 23 2020 at 09:18):

We can't do eigenvalues until Lean 4, because λ is a reserved symbol in Lean 3.

#### Mario Carneiro (May 23 2020 at 09:21):

I think it's reserved in lean 4 too :/

#### Patrick Massot (May 23 2020 at 09:25):

What? I thought this was gone. And you can override anything in Lean 4 so you can probably unreserve it

#### Patrick Massot (May 23 2020 at 10:14):

It doesn't say you can't unreserve it in favor of $\mapsto$

#### Kevin Buzzard (May 23 2020 at 10:27):

It's ok we can just fork

Last updated: Dec 20 2023 at 11:08 UTC