Real numbers
Content created by Egbert Rijke and malarbol.
Created on 2023-04-08.
Last modified on 2024-02-27.
Files in the real numbers folder
module real-numbers where open import real-numbers.dedekind-real-numbers public open import real-numbers.rational-real-numbers public
Recent changes
- 2024-02-27. malarbol. Rational real numbers (#1034).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).