Not Equal To

Stream: new members

[Dev-Indra]

Are there any theorems regarding not equals to in Lean, and if so what are some (with short description). Also what is the definition of not equal to in Lean?

[Bryan Gin-ge Chen]

See init.logic starting here. The theorems there are simple enough that you should be able to figure them out from the types themselves, but if you're confused, feel free to ask.

[Dev-Indra]

(deleted)

[Dev-Indra]

Thanks