Basic issue with importing BigOperators

Stream: new members

[Bernardo Anibal Subercaseaux Roa]

Hi! I've been importing different Mathlib files successfully, but upon doing import Mathlib.Algebra.BigOperators.Group.Finset I get error: 'Mathlib.Algebra.BigOperators.Group.Finset': no such file or directory, even though the file seems to exist. Is there something I need to install to make this work?

[Ruben Van de Velde]

No, that likely means the file really does not exist in the version of mathlib you're using

[Bernardo Anibal Subercaseaux Roa]

Thanks for your answer! But it's not clear to me how to deal with it then. My lakefile says

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

Is there a way to check "which version of mathlib" I'm using? or why is that the version I'm using doesn't have that file even though its here? [https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/Finset.html#BigOperators.bigsum]

[Ruben Van de Velde]

Check the lake-manifest.json

[Bernardo Anibal Subercaseaux Roa]

thanks! is there a command that updates it to the latest? or more to the point, what should I do upon experiencing this problem?

[Ruben Van de Velde]

See https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

Possibly the declaration you're looking for already exists but in a different file, and you could import that, but I'm not sure there's an easy way to discover that