Minimathlib A Lean 4 library of mathematics independent of Mathlib for autodidactic purposes. Expect stylistic blunders and unforced errors.