A Key Lean 4 Declarations
This appendix displays the formal Lean 4 code for the definitions and theorems claimed in the preceding chapters. Every declaration compiles against mathlib4 fde0cc5 with zero sorry.
This appendix displays the formal Lean 4 code for the definitions and theorems claimed in the preceding chapters. Every declaration compiles against mathlib4 fde0cc5 with zero sorry.