Where and how to find basic theorems?

Stream: lean4

[Sabbir Rahman]

Hello, I am a beginner trying to work with lean as a hobby. I started with lean4. If I understand correctly, It says here that standard library has the basic theorems proven. But what exactly are the names? For example, if I wanted to use commutativity of And what is the name of the theorem already proven? And in general what is the method to find the name or statement of these well-known theorems? Sorry if this is a too obvious question.

[Kevin Buzzard]

There's a naming convention #naming which will tell you that in Lean 3 the theorem will be called either and_comm or and.comm, and you can use #check to find out which. If you want to do mathematics you should stick to lean 3 but if you are doing logic or more CS related stuff then I should think lean 4 is fine, although it has different naming conventions -- try adding some capital letters

[Henrik Böving]

For Lean 4 what changes is: type names are in PascalCase and theorem names stay in snek_case so you if you want e.g. the theorem that for all natural numbers: 0 ≤ n you wanna search for Nat and then what the naming convention makes out of this theorem, in this case zero_le so we end up with Nat.zero_le

[Kyle Miller]

If you want to peruse the Lean 4 library, you can take a look at the Init section of https://leanprover-community.github.io/mathlib4_docs/ (Before that existed, I'd look through the source code directly, though I still do that to see how certain things are written.)