P → P — A proposition implies itself. ## Resource Links - Tactics used: - LeanNotes coding idioms used: [[exact-show]] - Video: - Lean file: - Github repo: - Used in: - [[Sheet1.lean|Formalising Mathematics-Section01-Logic, Sheet1]] ## Notes Foo ## Copyright, Authors, and README info ### Copyright and author credits Copyright (c) 2025 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta, Kevin Buzzard, Den Ducoff, Gemini 3.5 ### Read Me First This file is written in the [[LeanNotes coding style]] Links to: [[Law of Identity#Resource Links|Resources]] [[Law of Identity#Copyright, Authors, and README info|Copyright, Authors, and README info]]