Author : Christopher Schmidt

Date : 16.02.23

Includes the Lean Code ragarding this theorem.

Includes the Lean Code regarding this lemma shown in the Thesis.

Includes the complete Lean Code regarding this lemma and some other useful stuff.

Includes the Lean Code shown in the thesis to explain dependent type theory.

Moritz Firsching contributed to the Code contained in "Binomial Coefficients are (almost) never Powers". His Repository "formal_book" (https://github.com/mo271/formal_book) uses the here shown code and ideas (and most likely embodys a newer version).

This repository is archived.