Skip to content

Fill in some sorrys in Regularized.lean#21

Merged
Timeroot merged 2 commits intoTimeroot:mainfrom
MrBrain295:patch-1
Mar 3, 2026
Merged

Fill in some sorrys in Regularized.lean#21
Timeroot merged 2 commits intoTimeroot:mainfrom
MrBrain295:patch-1

Commits

Commits on Feb 8, 2026