From a0e19c357c679d29cc7b4b49a9738743c36bf11f Mon Sep 17 00:00:00 2001 From: malarbol Date: Sat, 24 Feb 2024 17:37:45 +0100 Subject: [PATCH] Update src/real-numbers/rational-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- src/real-numbers/rational-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index ad7c8ca9df..49c248a2a1 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -38,7 +38,7 @@ open import real-numbers.dedekind-real-numbers ## Idea -The type of rationals `ℚ` embeds into the type of Dedekind reals `ℝ` +The type of [rationals](elementary-number-theory.rational-numbers.md) `ℚ` [embeds](foundation-core.embeddings.md) into the type of [Dedekind reals](real-numbers.dedekind-real-numbers.md) `ℝ`. We call numbers in the [image](foundation.images.md) of this embedding {{#concept "rational real numbers" Agda=Rational-ℝ}}. ## Definitions