Zulip Chat Archive

Stream: new members

Topic: unknown identifier in challenge 8

Ameji B (Mar 01 2022 at 19:37):

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 (Mar 01 2022 at 19:38):

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 (Mar 01 2022 at 19:43):

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

Ameji B (Mar 01 2022 at 19:44):

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

Ameji B (Mar 01 2022 at 19:45):

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

Martin Dvořák (Mar 01 2022 at 19:45):

It doesn't build as is?

Ameji B (Mar 01 2022 at 19:46):

I get unknown identifier 'group'

Martin Dvořák (Mar 01 2022 at 19:47):

Do you import this file in the header?

Martin Dvořák (Mar 01 2022 at 19:50):

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

Martin Dvořák (Mar 01 2022 at 19:51):

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 (Mar 01 2022 at 19:51):

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

Ameji B (Mar 01 2022 at 19:51):

Thank you

Martin Dvořák (Mar 01 2022 at 19:51):

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

Martin Dvořák (Mar 01 2022 at 19:52):

The file group_theory.basic doesn't exist anymore.

Patrick Massot (Mar 01 2022 at 20:14):

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 (Mar 01 2022 at 21:28):

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.

Last updated: Dec 20 2023 at 11:08 UTC