Init Mathlib.Analysis.NormedSpace.Basic Mathlib.Analysis.Inn

Stream: mathlib4

[Lewis]

How to fix the error

Init Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Data.Matrix.Basic Mathlib.LinearAlgebra.FiniteDimensional.Defs` failed:

when importing like

import Mathlib.Analysis.Normed.Module.Basic


import Mathlib.Analysis.InnerProductSpace.Basic


import Mathlib.Data.Matrix.Basic

import Mathlib.LinearAlgebra.FiniteDimensional.Defs

?

Thanks.

[Yaël Dillies]

Analysis.NormedSpace.Basic was recently renamed to Analysis.Normed.Module.Basic

[Lewis]

Yaël Dillies said:

Analysis.NormedSpace.Basic was recently renamed to Analysis.Normed.Module.Basic

Tried "import Mathlib.Analysis.Normed.Module.Basic", but why does it still have errors? Thanks.

[Jireh Loreaux]

Is the error the same or different? Did you get the cache?

[Lewis]

Jireh Loreaux said:

Is the error the same or different? Did you get the cache?

Where is the "cache"? Thanks

[Lewis]

How to fix this error:

.elan/toolchains/leanprover--lean4---v4.11.0-rc2/bin/lake setup-file /home/codespace/Desktop/mathematics_in_lean/cs.lean Init Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Data.Matrix.Basic Mathlib.LinearAlgebra.FiniteDimensional.Defs` failed:

? Thanks a lot.

[Kim Morrison]

It seems you are only posting fragments of the error messages. To help you, you'll need to explain what command you are running, and the full output.