by_contradiction

Stream: new members

[Rajiv]

I am working through the book Logic and Proof to learn Lean. In section for Proof By Contradiction, it seems like by_contradiction is defined as ∀ {p : Prop}, (¬p → false) → p. Does lean have contradiction definition with the signature ∀ {p : Prop}, (p → false) → ¬p?

[Aniruddh Agarwal]

nevermind, I can't read

[Alex J. Best]

¬p is by definition p → false.

[Rajiv]

Thanks @Alex J. Best .