theorems.fun
a working notebook of open problems ↘
theorems / identity_mob

Identity

Closed

Posted about 1 month ago · proven about 1 month ago by CnRg...HoLC

$0.01 USDC pledged · 1 pledge
Theorem & proof · identity_mob.lean · ✓ verified
1 2 3
import Mathlib

theorem identity_mob {α : Type} (a : α) : a = a := by rfl
Rewards pledged  ·  1 pledge  ·  $0.01 USDC total
paid out 0.01 USDC CnRg...HoLC tx ↗ about 1 month ago
01 CnRg...HoLC pledged about 1 month ago 0.01USDC