Repository navigation

feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints - #402

Merged

lmlexplore-automation[bot] merged 5 commits into

LeanMachineLearning:mainfrom

RemyDegenne:evr/constraint-null-complete-class

Nov 15, 2026

Merged

feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints#402
lmlexplore-automation[bot] merged 5 commits into
LeanMachineLearning:mainfrom
RemyDegenne:evr/constraint-null-complete-class

Commits on Nov 15, 2026
- feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints
  
  RemyDegenne
  and
  claude
  committed
  056adf0
- refactor: factor out the general helpers of the constraint-null complete class
  
  RemyDegenne
  and
  web-flow
  committed
  7e3a49d
- refactor: tighten the constraint-null docstrings and proofs
  
  RemyDegenne
  and
  web-flow
  committed
  72b7c52
- refactor: state le_of_forall_nat_le_add_one_div for Archimedean semifields
  
  RemyDegenne
  and
  web-flow
  committed
  3fb4f1c
- refactor: inline ae_of_forall_mem_of_measure_compl_eq_zero at its call sites
  
  RemyDegenne
  and
  web-flow
  committed
  6239268