Commit 2026-04-11 09:33 048a4e7c

View on Github →

chore: move Archimedean to a new Defs file (#33894) I've also moved the most basic theorems (exists_nat_lt, etc.) to this file. This greatly decreases the imports needed to use these classes.

Estimated changes

deleted theorem exists_int_ge
deleted theorem exists_int_gt
deleted theorem exists_int_le
deleted theorem exists_int_lt
deleted theorem exists_lt_pow
deleted theorem exists_nat_ge
deleted theorem exists_nat_gt
deleted theorem exists_pow_lt
added theorem exists_int_ge
added theorem exists_int_gt
added theorem exists_int_le
added theorem exists_int_lt
added theorem exists_lt_pow
added theorem exists_nat_ge
added theorem exists_nat_gt
added theorem exists_pow_lt