The library documents itself · Numeric & optimization

stzMathClaimSet

12 own methods · 1 forms written with extensions, listed under their method

the source: base/math/stzMathClaim.ring(opens in a new tab) · All classes · The area reference: Numeric & optimization

Under each method, its extensions (Q CS XT Z ZZ IB W U): bold and ticked, it exists; struck, it does not. The extensions and what they mean

Examples: 0 come from the library's tests; 5 were composed from each method's signature and run for this page, on a fresh object, for example o1 = new stzMathClaimSet("a tampered lesson"). 7 methods have none yet. Examples run on 2026-10-03 12:54 inside the library at commit 0e72e2e2c.

Method

Explanation, as the source carries it

init

(no comment in the source: the name reads as a sentence) initno extension

Lesson

(no comment in the source: the name reads as a sentence) lesson

composed example

o1 = new stzMathClaimSet("a tampered lesson")
? o1.Lesson()
#--> a tampered lesson

composed from the signature, run for this page

no extension

Add

(no comment in the source: the name reads as a sentence) addQCSXTZZZIBWU

Claims

(no comment in the source: the name reads as a sentence) claimsno extension

Count

(no comment in the source: the name reads as a sentence) count

composed example

o1 = new stzMathClaimSet("a tampered lesson")
? o1.Count()
#--> 0

composed from the signature, run for this page

no extension

ToLean

one .lean file: Mathlib, the lesson, every theorem; names made unique by position

composed example

o1 = new stzMathClaimSet("a tampered lesson")
? o1.ToLean()
#--> -- a tampered lesson: 0 claim(s) emitted by stzMathClaimSet (plane stzlib-math, M6)
#--> -- check with: lake env lean <this file>   inside a Lake project holding Mathlib
#--> import Mathlib

composed from the signature, run for this page

no extension

WriteLean

(no comment in the source: the name reads as a sentence) write leanno extension

Diagnostics

the floor over every claim, in the house rule shape: a false claim is an errorno extension

Report

(no comment in the source: the name reads as a sentence) reportno extension

IsSound

(no comment in the source: the name reads as a sentence) is sound

composed example

o1 = new stzMathClaimSet("a tampered lesson")
? o1.IsSound()
#--> 1

composed from the signature, run for this page

no extension

CheckWithLean

through the door, once for the whole fileno extension

Why

(no comment in the source: the name reads as a sentence) why

composed example

o1 = new stzMathClaimSet("a tampered lesson")
? o1.Why()
#--> the claims of 'a tampered lesson': 0 statement(s), 0 false on the numeric floor; the Lean door is open

composed from the signature, run for this page

no extension