Change of Basis confusion

Stream: new members

[Alex Brodbelt]

Is this true or am I misinterpreting what Basis.toMatrix does?
I can't find this in mathlib and I feel like it should be there if it is true

import Mathlib

open Matrix

lemma foo (ι : Type u_1) [Fintype ι] (R : Type u_3) [CommSemiring R] [Module R (ι → R)]
  (b b' : Basis ι R (ι → R)) (i : ι):
   b.toMatrix b' *ᵥ (b' i) = b i := by sorry

[Eric Wieser]

This doesn't look true to me

[Eric Wieser]

Maybe it's true for an orthonormal basis, or when one or both bases are Pi.basisFun

[Alex Brodbelt]

Hmm, what is the equivalent of the following result in Lean?

Let $\mathcal{B}$, $\mathcal{B}'$ be indexed basis of the vector space $V$, let f be an endomorphism of $V$, and let $v \in V$ then

\prescript{\mathcal{B}}{{[f(v)]}} = \prescript{\mathcal{B}}{[f]_{\mathcal{B}'}} \prescript{\mathcal{B}'}{[v]}

(apologies, I can't get the Latex to render)

I thought the above was this result?

[Kevin Buzzard]

Something like this should certainly be true

[llllvvuu]

Maybe docs#Basis.toMatrix_mulVec_repr?

[Kevin Buzzard]

docs#Basis.toMatrix_mulVec_repr

[Alex Brodbelt]

Hmm, strange I could not find this... Thank you

Currently I get the error "unknown constant 'Basis.toMatrix_mulVec_repr' "

I am importing all of mathlib, have done update lake and tried updating dependencies and so on. I have clicked all buttons known to me.

It does indeed work in the playground, but when I copy the exact same code to my own project it doesn't recognize it. :thinking:

Do any of you recognize this problem?

[Alex Brodbelt]

just copied over proof of mathlib for now

[Eric Wieser]

What version of mathlib is in your lake-manifest.json?

[Alex Brodbelt]

I have the version e3e46c381d49179c3818135c0a888bc69a958de3

[Alex Brodbelt]

I don't need the theorem above in the end, but I can't access some other theorems that I do definitely need.

[Alex Brodbelt]

Is there somewhere I can read about fixing the mathlib dependency?

[Kevin Buzzard]

Are you working in mathlib itself or in a project which depends on mathlib?

[Alex Brodbelt]

I'm working on a project that depends on mathlib. I.e: made my own repo using Project: Create Project Using Mathlib...

[Kevin Buzzard]

So use VS Code to "update dependencies" but note that this could well break your code as well as updating mathlib. I update the FLT project around once a week.

[Alex Brodbelt]

Ah yes... I remember trying this but getting the nasty error like:

Cannot update dependency. Command output: trace: ././.lake/packages/mathlib> git fetch --tags --force origin info: leanprover-community/mathlib: updating repository '././.lake/packages/mathlib' to revision '9419c034110d02f83c8cf286f877c624e492e16f' trace: ././.lake/packages/mathlib> git checkout --detach 9419c034110d02f83c8cf286f877c624e492e16f -- trace: stderr: Previous HEAD position was e3e46c381d feat: ‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖ (#18005) HEAD is now at 9419c03411 chore(CategoryTheory/Adjunction/Opposites): redefine the opposite of an adjunction (#20375) trace: ././.lake/packages/batteries> git fetch --tags --force origin info: batteries: updating repository '././.lake/packages/batteries' to revision 'f007bfe46ea8fb801ec907df9ab540054abcc5fd' trace: ././.lake/packages/batteries> git checkout --detach f007bfe46ea8fb801ec907df9ab540054abcc5fd -- trace: stderr: Previous HEAD position was dd6b1019 chore: rename List.modifyNth->modify and insertNth->insertIdx (#1003) HEAD is now at f...

[Alex Brodbelt]

where the process proceeds to die starts at:

[Error - 3:08:00 PM] Request textDocument/completion failed.
  Message: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)
  Code: -32603

[Alex Brodbelt]

Is it a bad idea to set maxHeartbeats to 0?

[Alex Brodbelt]

I'll let you know how this goes :clown:

[Alex Brodbelt]

Still fails : (

[Ruben Van de Velde]

Try moving the .lake folder somewhere else (or deleting it) and then run the update command again