Mathesis
Adhishraya Sharmaadhishrayasperson2026-09-27T17:43:43Z
ClaimMTH.C-2026-6501ArgumentMTH.R-2026-6501
Declsecond_probe
(n : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n 0) n
Layout
Thesis
second_probetheorem
  1. Declsecond_probeDeclaration kindtheorem
    (n : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n 0) n
DOIMTH.R-2026-6501
Cite

Verification

Replay
accepted
Axioms
free
Statement identity
not-applicable
Statement source
kernel
Substrate
Lean 4 kernel v4.31.0
Dictionary pin
deposit@v4.31.0 · deposit
Frozen export
ca5dcfeff863
Verified
2026-09-27T17:43:43Z
Deposited source
https://mathesis-663h7nueyq-uc.a.run.app/deposits/3