classes

Stream: new members

[Lucas]

Hi, I am trying to formalize some (basic) theorems about prime numbers, and the definition includes the definition irreducible, which appears to be a class. I don't know anything about classes in lean, and the lean reference manual 4.10 just links to some 1994 paper and that's it. Where is documentation about classes in lean, and how do you use irreducible p in a proof?

[Alex J. Best]

Check out https://leanprover.github.io/theorem_proving_in_lean/type_classes.html, its quite often a more helpful resource than the reference manual.

[Lucas]

cool, this looks like exactly what I was looking for