Schlessinger’s criterion

1 Introduction

The goal of this project is to formalize Schlessinger’s criterion in Lean following the original article [ . Some parts are also based on the proof given in [ .