Order of the generator of a Finite Cyclic Group

Stream: maths

[Zillion Demor]

I am just getting started with Lean. I have been trying to learn Lean4 using LLMs, but it looks like Lean4 is very newer than and different to Lean3, so, their responses are all out of date. Can someone prove this simple thing?
"The order of a generator of a finite cyclic group G is the same as the cardinality of the group G"

[Josha Dekker]

I think using LLMs to learn Lean is generally discouraged because of the quickly evolving nature of certain aspects of Lean/Mathlib. Instead, you may want to consider the resources here: https://leanprover-community.github.io/learn.html

[Kevin Buzzard]

Did you try moogle.ai ?

[Zillion Demor]

@Kevin Buzzard Sir Dr. Kevin, I have found that leansearch.net is better than moogle.ai in this particular case, at least. The former returned the right theorem as the first result, but the theorem was nowhere to be seen in moogle.ai's results

[Aaron Hill]

leansearch.net is currently giving me a 503 error - do you remember what the name of the theorem was?

[Aaron Hill]

Found it: orderOf_generator_eq_natCard