SimpleGraph is not recognised

Stream: new members

[Tomer]

Hello, I am new here so I am sorry if I missed something.

I am working on a project where I need to work with random graphs, for that my plan is to define a random variable on the set of possible simple graphs, but whenever I try to use SimpleGraph there is an error saying it is an Unknown Identifier. Sorry it is a bit vague, I am not sure what to detail about.

Thank you, Tomer

[Julian Berman]

Welcome. It's easier to answer questions if you make them an #mwe (that's a link you can click). In particular sharing exactly what code you ran to get the message you're mentioning is the way to make your question less vague.

[Julian Berman]

That being said, you're probably missing an import Mathlib in what you're running, or you can use a more specific import like import Mathlib.Combinatorics.SimpleGraph.Walk but then you'll need to potentially add more imports if you start using things from other modules.

[Julian Berman]

Here's an example you can see working by clicking on the live web playground link that will show up if you hover your mouse over this code block here in Zulip:

import Mathlib
#check SimpleGraph

[Yaël Dillies]

Hey! Out of curiosity, what kind of random graphs are you interested in?

[Tomer]

Sorry on the question, I accidentally imported only Mathlib.tactics, instead of the whole of mathlib so that was the problem, I am still stuck on trying to understand how to make the set of the simple graphs but that a different problem, I defiantly feel like I miss something in using the existing simple graph definition in defining this set.

As for which random graph I try to make, simply trying to make G(n,p).

[Yaël Dillies]

Great :) G(n, p) is defined in #31364

[Tomer]

Thank you, it seems it is a new one which explains why it was so hard to find.