Theorem Marketplace

Theorem Details

-- Both the bounty and the submission should be valid Lean files
-- In the bounty, you can replace the entire proof (or anything else) with a sorry
-- In the submissions, all sorries should be defined

theorem self_eq_self (n : Nat) : 10 * n = 10 * n :=
  sorry

Bounty: 0.003 ETH

Status: Closed

Proof

theorem self_eq_self (n : Nat) : 10 * n = 10 * n :=
  rfl

Back to Bounties