unknown identifier in challenge 8

Stream: new members

[Ameji B]

Hi all, I came here from this list of challenges in lean. The 8th one uses group theory but I get " unknown identifier 'group' ".

[Ameji B]

I haven't had this problem with any of the other challenge files, all of them had appropriate imports. I tried import group_theory but it looks like I have to choose something more specific than that? But there is nothing like group_theory.basic

[Martin Dvořák]

Post a relevant part of the code, please. I don't know what is the 8th challenge.

[Ameji B]

example (G : Type) [group G] (g h k : G) : (g * h * k⁻¹)⁻¹ = k * h⁻¹ * g⁻¹ :=
begin
  sorry
end

[Ameji B]

every other challenge has an import except this one
challenges are here: https://cocalc.com/share/public_paths/f014cd1885a22e8665a728be825e563fc79b7e1f/README.md

[Martin Dvořák]

It doesn't build as is?

[Ameji B]

I get unknown identifier 'group'

[Martin Dvořák]

Do you import this file in the header?
https://github.com/leanprover-community/mathlib/blob/3007f24ccfa0c1235e3ad6b355e331c2da88e07c/src/algebra/group/defs.lean

[Martin Dvořák]

It seems that the definition of a group was moved from algebra/group/basic to algebra/group/defs in 2020.

[Martin Dvořák]

It seems that your problem is already in the first part of the path, assuming that you are using the current version of mathlib.

[Ameji B]

I imported algebra.group.basic and that worked ^^

[Ameji B]

Thank you

[Martin Dvořák]

Oh yes.Because algebra/group/basic imports algebra/group/defs so you get it transitively.

[Martin Dvořák]

The file group_theory.basic doesn't exist anymore.

[Patrick Massot]

This list of challenge is ancient. If you try to use it with a modern mathlib you should expect a lot of issues.

[Kevin Buzzard]

I remember I put them there but I'm not sure I know how to update them and I also don't know which version of Lean cocalc is running right now.