Documentation

Pretty.Claims

Claimed results formalized in Lean #