P → P — A proposition implies itself. ## Resource Links - Tactics used: [[Tactics/intro-tactic|intro]], [[Tactics/exact-tactic|exact]], [[show-tactic]] - [[LeanNote idioms]] used: [[exact-show]] - Video: - Lean file: - Github repo: - Used in: - [[Sheet 1 - LeanNotes Solutions|Formalising Mathematics-Section01-Logic, Sheet1]] ## Notes ## 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 The Law-of-Identify.lean 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]]