Repository navigation

Prove some sorrys, update Mathlib - #38

Merged

RemyDegenne merged 10 commits into

mainfrom

Oct 23, 2025

Merged

Prove some sorrys, update Mathlib#38
RemyDegenne merged 10 commits into
mainfrom
work

Commits on Oct 21, 2025
- add adapted_hist
  RemyDegenne
  committed
  c621be8
- add iIndepFun lemma
  RemyDegenne
  committed
  4ac1eaa
- easy implication done
  RemyDegenne
  committed
  8816659
- refine -> exact
  RemyDegenne
  committed
  309953d
Commits on Oct 23, 2025
- prove last sorry in the ETC file
  RemyDegenne
  committed
  13a5a54
- extract MeasurableSet lemmas
  RemyDegenne
  committed
  a256979
- prove stepsUntil_eq_congr
  RemyDegenne
  committed
  9ce572e
- move lemmas
  RemyDegenne
  committed
  9b935db
- bump
  RemyDegenne
  committed
  b7e28e4
- extract lemma
  RemyDegenne
  committed
  1f96276