object file '././.lake/packages/mathlib/.lake/build/lib/Math

Stream: mathlib4

[Lewis]

Why does it say "object file '././.lake/packages/mathlib/.lake/build/lib/Mathlib/LinearAlgebra/Matrix.olean' of module Mathlib.LinearAlgebra.Matrix does not exist" when running "import Mathlib.LinearAlgebra.Matrix"? Thanks.

[Edward van de Meent]

possibly because that isn't a lean file?

[Edward van de Meent]

you might be looking for Mathlib.Data.Matrix.Basic?

[Lewis]

Edward van de Meent said:

possibly because that isn't a lean file?

Isn't there a folder at https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/LinearAlgebra ? Thanks

[Edward van de Meent]

there is, but i don't know that you can import a folder...

[Lewis]

Edward van de Meent said:

there is, but i don't know that you can import a folder...

Thanks; Could you please help fix this error "object file '././.lake/packages/mathlib/.lake/build/lib/Mathlib/Analysis/NormedSpace/FiniteDimensional.olean' of module Mathlib.Analysis.NormedSpace.FiniteDimensional does not exist"? Thanks a lot.

[Edward van de Meent]

that's not a file either?

[Edward van de Meent]

did you mean Mathlib.Analysis.NormedSpace.FiniteDimension?

[Lewis]

Edward van de Meent said:

that's not a file either?

How to know what files to import in the beginning of a lean file that one writes? Thanks.

[Edward van de Meent]

if you make sure your version of mathlib is current, search for the statement you want at the docs, then the file you need to import to make it available is at the top of the page in bold

[Lewis]

Edward van de Meent said:

if you make sure your version of mathlib is current, search for the statement you want at the docs, then the file you need to import to make it available is at the top of the page in bold

Then what should one import if one wants to use probability_mass_function.normal ? and why does searching there not produce any search result? Thanks.

[Eric Wieser]

Or use import Mathlib to just get everything, then use #min_imports to cut them back when you're done

[Eric Wieser]

Then what should one import if one wants to use probability_mass_function.normal ? and why does searching there not produce any search result? Thanks.

What makes you think this exists in the first place, if search didn't find it?

[Lewis]

Eric Wieser said:

Then what should one import if one wants to use probability_mass_function.normal ? and why does searching there not produce any search result? Thanks.

What makes you think this exists in the first place, if search didn't find it?

Then how to search there if one wants to use singular value decomposition? Thanks.

[Lewis]

Eric Wieser said:

Or use import Mathlib, then use #min_imports to cut them back when you're done

How to import if one wants to use singular value decomposition ? Thanks.

[Yaël Dillies]

Where do you get these names from?

[Yaël Dillies]

What makes you think that Mathlib contains singular value decomposition?

[Lewis]

Yaël Dillies said:

Where do you get these names from?

Why should Mathlib4 not contain one of the essentials of linear algebra, singular value decomposition? If Mathlib4 does not contain singular value decomposition, is there an easy way to use singular value decomposition in Lean 4? Thanks.

[Edward van de Meent]

Mathlib might contain the lemma you want, but not under the name you expect. are you simply guessing the name?

[Yaël Dillies]

Lewis said:

Why should Mathlib4 not contain one of the essentials of linear algebra, singular value decomposition?

Long story short, the answer is "#6042 has not yet been merged"