Theorem Details
import Mathlib
theorem self_eq_self (n : Nat) : n = n := sorry
Bounty: 0.0013 ETH
Status: Closed
Proof
import Mathlib theorem self_eq_self (n : Nat) : n = n := rfl
import Mathlib theorem self_eq_self (n : Nat) : n = n := sorry
Bounty: 0.0013 ETH
Status: Closed
import Mathlib theorem self_eq_self (n : Nat) : n = n := rfl