| [[Identity]] | P → P, ¬P → ¬P | A proposition is equal to itself. | | | ------------ | -------------- | --------------------------------- | --- | - Lean file - Notable Tactics: FOO - LeanNotes idioms: [[exact-show]], [[intro-typing]] - GitHub: FOO - See also: - [[Courses and eBooks/Formalising Mathematics - Metha/Table of Contents|Formalising Mathematics-Section01-Logic, Sheet1]] - Example (3) - Video - FOO ## Authors [[Bhavik Mehta]], [[Kevin Buzzard]], [[dducoff|Den Ducoff]], [[Gemini 3.5]] ## Copyright Portions of this work are derived from [Course notes for Formalising Mathematics 2026](https://github.com/b-mehta/formalising-mathematics-notes) Copyright (c) 2025 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file [LICENSE ](https://github.com/b-mehta/formalising-mathematics-notes/blob/main/LICENSE). --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-08-18