Commit 2026-01-29 14:55 d51f24ac

View on Github →

feat: ring where elements are bounded by naturals is a floor ring (#34560) Used in the CGT repo.

Estimated changes

added theorem exists_floor'