import algebra.group

Stream: new members

[Dionysis Zindros]

I'm trying to import algebra.group in VS code. I get the error: file 'init' not found in the search path. I'm using an M1 mac. I've initialized my lean project and ensured mathlib is installed by using leanproject new. I have started VS code from within the folder. I think my leanpkg.path and leanpkg.toml, as well as my project structure looks good. I've also exported LEAN_PATH from my terminal to include both the mathlib src and the project src directory.

I'm trying to reproduce the examples in this documentation page: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#using-the-library

It seems that there is no folder named _target/deps/mathlib/algebra/group in my project. Did something change from version to version? Thanks!

[Yaël Dillies]

algebra.group has been renamed to algebra.group.basic a loong time ago! Expect examples in TPIL to be outdated.

[Kevin Buzzard]

I think Jeremy has been good at keeping TPIL up to date!

[Yaël Dillies]

All the imports in section 6 are outdated, though. It's not too hard to fix each, but they are currently wrong.

[Kevin Buzzard]

PRs welcome!

[Yaël Dillies]

https://github.com/leanprover/theorem_proving_in_lean/pull/119

[Yaël Dillies]

@Dionysis Zindros, all imports have now been fixed thanks to Jeremy Avigad's quick response.