Repository navigation

Generalize finenum sample space - #48

Merged

marekpetrik merged 9 commits into

mainfrom

generalize-finenum-sample-space

Sep 4, 2026

Merged

Generalize finenum sample space#48
marekpetrik merged 9 commits into
mainfrom
generalize-finenum-sample-space

Commits on Jul 29, 2026
- Generalize probability space from Fin n to any [FinEnum Ω]
  marekpetrik
  committed
  3f98d8b
Commits on Aug 6, 2026
- updated mathlib version
  marekpetrik
  committed
  2f35d9b
- Cleaned up some warnings regarding Finenum class and unnecessary lemmas
  marekpetrik
  committed
  aaff979
Commits on Aug 20, 2026
- simplified claude's proof
  marekpetrik
  committed
  e8978e5
Commits on Aug 24, 2026
- added a nonempty attribute to Omega
  marekpetrik
  committed
  a54fa58
Commits on Aug 25, 2026
- simplified and cleaned up
  marekpetrik
  committed
  22c0c89
Commits on Sep 4, 2026
- simplified maxima and minima
  marekpetrik
  committed
  e6a2d8d
- added the latex file back into the project
  marekpetrik
  committed
  0a3c2d7
- CI: build library, API docs, and LaTeX paper; publish docs to GitHub Pages
  marekpetrik
  committed
  4365fef