can't import "data.nat.modeq"

Stream: lean4

[TAWSIF AHMED]

relatively new in Lean. I believe importing a package is Lean3 behaviour. Unfortunately after searching almost all existing materials on the internet I wasn't able to understand how it fix this error on lean4.

I read the documentation for mathslib3 but couldn't understand how it can be used in Lean4. That's why, if someone could help, that'll be really appreciated. [I have mathslib installed via pip]

Code:

import data.nat.modeq

theorem fermat_little_theorem (p : ℕ) (hp_prime : nat.prime p) (a : ℕ) : a^p ≡ a [MOD p] :=
begin
  exact nat.modeq.modeq_pow_eq_modeq hp_prime (nat.modeq.refl a),
end

Error: unknown package 'data'

[Kyle Miller]

In mathlib4, the module is now Mathlib.Data.Nat.ModEq

[Kevin Buzzard]

(deleted)

[Kyle Miller]

(deleted)

[Kyle Miller]

I haven't tested it, but that Lean 3 syntax would need to be translated to Lean 4 and the new Mathlib 4 names like such:

theorem fermat_little_theorem (p : ℕ) (hp_prime : Nat.Prime p) (a : ℕ) : a^p ≡ a [MOD p] := by
  exact Nat.ModEq.modEq_pow_eq_modEq hp_prime (Nat.ModEq.refl a)

Again, I didn't test it at all, but the point is that it needs translation.

[TAWSIF AHMED]

Kyle Miller said:

I haven't tested it, but that Lean 3 syntax would need to be translated to Lean 4 and the new Mathlib 4 names like such:

theorem fermat_little_theorem (p : ℕ) (hp_prime : Nat.Prime p) (a : ℕ) : a^p ≡ a [MOD p] := by
  exact Nat.ModEq.modEq_pow_eq_modEq hp_prime (Nat.ModEq.refl a)

Again, I didn't test it at all, but the point is that it needs translation.

thanks for the help! and heads -up

[TAWSIF AHMED]

I tried to import the module as Mathlib.Data.Nat.ModEq by writing import Mathlib.Data.Nat.ModEq and it says, no package found named Mathlib. Why that might be causing? you think : )

Kyle Miller said:

In mathlib4, the module is now Mathlib.Data.Nat.ModEq

[Kevin Buzzard]

Because you're not using a correctly set-up project which has mathlib as a dependency?

[Kevin Buzzard]

Go to the community website and read about how to correctly set up a lean 4 project with mathlib as a dependency.

[Jireh Loreaux]

I believe Kevin is referring to this page.

[TAWSIF AHMED]

Kevin Buzzard said:

Because you're not using a correctly set-up project which has mathlib as a dependency?

I have installed Lean4 via VS Code extension. And Mathslib library through git and pip I also suspected it might be that Lean4 wasn't able to find Mathslib after I installed it using pip so same thing I know, I still installed the library using my terminal as well. Still the problem remains. Do you have any suggestion on what might have gone wrong?

OS: Windows 11

[Arthur Paulino]

How did you end up using pip for Lean 4 setup? AFAIK, Python is out of the loop in the current Lean 4 dev environment

[Arthur Paulino]

I'm asking this because apparently you're still following a flawed tutorial

[James Gallicchio]

(If there is a tutorial that says to use pip, let us know so we can update it! :big_smile:)

[TAWSIF AHMED]

Arthur Paulino said:

How did you end up using pip for Lean 4 setup? AFAIK, Python is out of the loop in the current Lean 4 dev environment

I had searched for "How to install Lean4?" on Google at first before reading the documentation. And in that video from YouTube Channel "LeanProver" most likey, they demonstrated the installation process via VS Code extension and Mathslib library via python.

I actually resorted to a video for installation as it was really confusing how to install Lean, at the first place. Because there were so many websites, notes and materials that it's hard to understand, which one is the updated source/official source.

I believe, Lean, should take a python approach and list all its previous versions and their documentations in one place, to avoid confusion. Otherwise it is difficult in the sense, many individuals/old projects still use previous versions of Lean and each time there's a version update Lean, ends-up creating a new website, which adds more to the confusion.

[TAWSIF AHMED]

Arthur Paulino said:

I'm asking this because apparently you're still following a flawed tutorial

I also believe the same case. I had replied to your previous message and explained where I found the learning materials

[TAWSIF AHMED]

James Gallicchio said:

(If there is a tutorial that says to use pip, let us know so we can update it! :big_smile:)

this was the video, I followed before seeing the documentation. Video link: https://www.youtube.com/watch?v=y3GsHIe4wZ4

[Scott Morrison]

Your message is misformatted so we can't click the link: https://www.youtube.com/watch?v=y3GsHIe4wZ4

[Scott Morrison]

That is very old, and about Lean 3.

[Scott Morrison]

I will see if I can change the title now.

[Scott Morrison]

Okay, I have unlisted this, hopefully it will not show up in search results anymore.

[Marc Huisinga]

Scott Morrison said:

Okay, I have unlisted this, hopefully it will not show up in search results anymore.

Pointing to the new Lean 4 installation instructions in the description may also be a good idea so that people following any straggler URLs to the video are immediately led to the right place

[Marc Huisinga]

Also note that the video can still be found by going through Playlists > Tutorial videos