Skip to content

Prove some admitted lemmas in experimental_reals - #2007

Merged
affeldt-aist merged 4 commits into
math-comp:masterfrom
ethanlee515:experimental-reals-fixes
Jul 28, 2026
Merged

Prove some admitted lemmas in experimental_reals#2007
affeldt-aist merged 4 commits into
math-comp:masterfrom
ethanlee515:experimental-reals-fixes

Simplify `interchange_psum` proof

e69686a
Select commit
Loading
Failed to load commit list.
Sign in for the full log view