Documentation

Mathlib.NumberTheory.Zsqrtd.Basic

ℤ[√d] #

The ring of integers adjoined with a square root of d : ℤ.

After defining the norm, we show that it is a linearly ordered commutative ring, as well as an integral domain.

We provide the universal property, that ring homomorphisms ℤ√d →+* R correspond to choices of square roots of d in R.

structure Zsqrtd (d : ) :

The ring of integers adjoined with a square root of d. These have the form a + b √d where a b : ℤ. The components are called re and im by analogy to the negative d case.

  • re :

    Component of the integer not multiplied by √d

  • im :

    Component of the integer multiplied by √d

Instances For
    theorem Zsqrtd.ext_iff {d : } {x y : ℤ√d} :
    x = y x.re = y.re x.im = y.im
    theorem Zsqrtd.ext {d : } {x y : ℤ√d} (re : x.re = y.re) (im : x.im = y.im) :
    x = y
    def instDecidableEqZsqrtd.decEq {d✝ : } (x✝ x✝¹ : ℤ√d✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For

      The ring of integers adjoined with a square root of d. These have the form a + b √d where a b : ℤ. The components are called re and im by analogy to the negative d case.

      Equations
      Instances For
        def Zsqrtd.ofInt {d : } (n : ) :

        Convert an integer to a ℤ√d

        Equations
        Instances For
          theorem Zsqrtd.re_ofInt {d : } (n : ) :
          (ofInt n).re = n
          @[deprecated Zsqrtd.re_ofInt (since := "2025-08-31")]
          theorem Zsqrtd.ofInt_re {d : } (n : ) :
          (ofInt n).re = n

          Alias of Zsqrtd.re_ofInt.

          theorem Zsqrtd.im_ofInt {d : } (n : ) :
          (ofInt n).im = 0
          @[deprecated Zsqrtd.im_ofInt (since := "2025-08-31")]
          theorem Zsqrtd.ofInt_im {d : } (n : ) :
          (ofInt n).im = 0

          Alias of Zsqrtd.im_ofInt.

          instance Zsqrtd.instZero {d : } :

          The zero of the ring

          Equations
          @[simp]
          theorem Zsqrtd.re_zero {d : } :
          re 0 = 0
          @[deprecated Zsqrtd.re_zero (since := "2025-08-31")]
          theorem Zsqrtd.zero_re {d : } :
          re 0 = 0

          Alias of Zsqrtd.re_zero.

          @[simp]
          theorem Zsqrtd.im_zero {d : } :
          im 0 = 0
          @[deprecated Zsqrtd.im_zero (since := "2025-08-31")]
          theorem Zsqrtd.zero_im {d : } :
          im 0 = 0

          Alias of Zsqrtd.im_zero.

          Equations
          instance Zsqrtd.instOne {d : } :

          The one of the ring

          Equations
          @[simp]
          theorem Zsqrtd.re_one {d : } :
          re 1 = 1
          @[deprecated Zsqrtd.re_one (since := "2025-08-31")]
          theorem Zsqrtd.one_re {d : } :
          re 1 = 1

          Alias of Zsqrtd.re_one.

          @[simp]
          theorem Zsqrtd.im_one {d : } :
          im 1 = 0
          @[deprecated Zsqrtd.im_one (since := "2025-08-31")]
          theorem Zsqrtd.one_im {d : } :
          im 1 = 0

          Alias of Zsqrtd.im_one.

          def Zsqrtd.sqrtd {d : } :

          The representative of √d in the ring

          Equations
          Instances For
            @[simp]
            theorem Zsqrtd.re_sqrtd {d : } :
            @[deprecated Zsqrtd.re_sqrtd (since := "2025-08-31")]
            theorem Zsqrtd.sqrtd_re {d : } :

            Alias of Zsqrtd.re_sqrtd.

            @[simp]
            theorem Zsqrtd.im_sqrtd {d : } :
            @[deprecated Zsqrtd.im_sqrtd (since := "2025-08-31")]
            theorem Zsqrtd.sqrtd_im {d : } :

            Alias of Zsqrtd.im_sqrtd.

            instance Zsqrtd.instAdd {d : } :

            Addition of elements of ℤ√d

            Equations
            @[simp]
            theorem Zsqrtd.add_def {d : } (x y x' y' : ) :
            { re := x, im := y } + { re := x', im := y' } = { re := x + x', im := y + y' }
            @[simp]
            theorem Zsqrtd.re_add {d : } (z w : ℤ√d) :
            (z + w).re = z.re + w.re
            @[deprecated Zsqrtd.re_add (since := "2025-08-31")]
            theorem Zsqrtd.add_re {d : } (z w : ℤ√d) :
            (z + w).re = z.re + w.re

            Alias of Zsqrtd.re_add.

            @[simp]
            theorem Zsqrtd.im_add {d : } (z w : ℤ√d) :
            (z + w).im = z.im + w.im
            @[deprecated Zsqrtd.im_add (since := "2025-08-31")]
            theorem Zsqrtd.add_im {d : } (z w : ℤ√d) :
            (z + w).im = z.im + w.im

            Alias of Zsqrtd.im_add.

            instance Zsqrtd.instNeg {d : } :

            Negation in ℤ√d

            Equations
            @[simp]
            theorem Zsqrtd.re_neg {d : } (z : ℤ√d) :
            (-z).re = -z.re
            @[deprecated Zsqrtd.re_neg (since := "2025-08-31")]
            theorem Zsqrtd.neg_re {d : } (z : ℤ√d) :
            (-z).re = -z.re

            Alias of Zsqrtd.re_neg.

            @[simp]
            theorem Zsqrtd.im_neg {d : } (z : ℤ√d) :
            (-z).im = -z.im
            @[deprecated Zsqrtd.im_neg (since := "2025-08-31")]
            theorem Zsqrtd.neg_im {d : } (z : ℤ√d) :
            (-z).im = -z.im

            Alias of Zsqrtd.im_neg.

            instance Zsqrtd.instMul {d : } :

            Multiplication in ℤ√d

            Equations
            @[simp]
            theorem Zsqrtd.re_mul {d : } (z w : ℤ√d) :
            (z * w).re = z.re * w.re + d * z.im * w.im
            @[deprecated Zsqrtd.re_mul (since := "2025-08-31")]
            theorem Zsqrtd.mul_re {d : } (z w : ℤ√d) :
            (z * w).re = z.re * w.re + d * z.im * w.im

            Alias of Zsqrtd.re_mul.

            @[simp]
            theorem Zsqrtd.im_mul {d : } (z w : ℤ√d) :
            (z * w).im = z.re * w.im + z.im * w.re
            @[deprecated Zsqrtd.im_mul (since := "2025-08-31")]
            theorem Zsqrtd.mul_im {d : } (z w : ℤ√d) :
            (z * w).im = z.re * w.im + z.im * w.re

            Alias of Zsqrtd.im_mul.

            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Zsqrtd.re_sub {d : } (z w : ℤ√d) :
            (z - w).re = z.re - w.re
            @[deprecated Zsqrtd.re_sub (since := "2025-08-31")]
            theorem Zsqrtd.sub_re {d : } (z w : ℤ√d) :
            (z - w).re = z.re - w.re

            Alias of Zsqrtd.re_sub.

            @[simp]
            theorem Zsqrtd.im_sub {d : } (z w : ℤ√d) :
            (z - w).im = z.im - w.im
            @[deprecated Zsqrtd.im_sub (since := "2025-08-31")]
            theorem Zsqrtd.sub_im {d : } (z w : ℤ√d) :
            (z - w).im = z.im - w.im

            Alias of Zsqrtd.im_sub.

            Equations
            • One or more equations did not get rendered due to their size.
            instance Zsqrtd.commRing {d : } :
            Equations
            • One or more equations did not get rendered due to their size.
            instance Zsqrtd.instStar {d : } :

            Conjugation in ℤ√d. The conjugate of a + b √d is a - b √d.

            Equations
            @[simp]
            theorem Zsqrtd.star_mk {d : } (x y : ) :
            star { re := x, im := y } = { re := x, im := -y }
            @[simp]
            theorem Zsqrtd.re_star {d : } (z : ℤ√d) :
            (star z).re = z.re
            @[deprecated Zsqrtd.re_star (since := "2025-08-31")]
            theorem Zsqrtd.star_re {d : } (z : ℤ√d) :
            (star z).re = z.re

            Alias of Zsqrtd.re_star.

            @[simp]
            theorem Zsqrtd.im_star {d : } (z : ℤ√d) :
            (star z).im = -z.im
            @[deprecated Zsqrtd.im_star (since := "2025-08-31")]
            theorem Zsqrtd.star_im {d : } (z : ℤ√d) :
            (star z).im = -z.im

            Alias of Zsqrtd.im_star.

            Equations
            @[simp]
            theorem Zsqrtd.re_natCast {d : } (n : ) :
            (↑n).re = n
            @[deprecated Zsqrtd.re_natCast (since := "2025-08-31")]
            theorem Zsqrtd.natCast_re {d : } (n : ) :
            (↑n).re = n

            Alias of Zsqrtd.re_natCast.

            @[simp]
            theorem Zsqrtd.re_ofNat {d : } (n : ) [n.AtLeastTwo] :
            (OfNat.ofNat n).re = n
            @[deprecated Zsqrtd.re_ofNat (since := "2025-08-31")]
            theorem Zsqrtd.ofNat_re {d : } (n : ) [n.AtLeastTwo] :
            (OfNat.ofNat n).re = n

            Alias of Zsqrtd.re_ofNat.

            @[simp]
            theorem Zsqrtd.im_natCast {d : } (n : ) :
            (↑n).im = 0
            @[deprecated Zsqrtd.im_natCast (since := "2025-08-31")]
            theorem Zsqrtd.natCast_im {d : } (n : ) :
            (↑n).im = 0

            Alias of Zsqrtd.im_natCast.

            @[simp]
            theorem Zsqrtd.im_ofNat {d : } (n : ) [n.AtLeastTwo] :
            @[deprecated Zsqrtd.im_ofNat (since := "2025-08-31")]
            theorem Zsqrtd.ofNat_im {d : } (n : ) [n.AtLeastTwo] :

            Alias of Zsqrtd.im_ofNat.

            theorem Zsqrtd.natCast_val {d : } (n : ) :
            n = { re := n, im := 0 }
            @[simp]
            theorem Zsqrtd.re_intCast {d : } (n : ) :
            (↑n).re = n
            @[deprecated Zsqrtd.re_intCast (since := "2025-08-31")]
            theorem Zsqrtd.intCast_re {d : } (n : ) :
            (↑n).re = n

            Alias of Zsqrtd.re_intCast.

            @[simp]
            theorem Zsqrtd.im_intCast {d : } (n : ) :
            (↑n).im = 0
            @[deprecated Zsqrtd.im_intCast (since := "2025-08-31")]
            theorem Zsqrtd.intCast_im {d : } (n : ) :
            (↑n).im = 0

            Alias of Zsqrtd.im_intCast.

            theorem Zsqrtd.intCast_val {d : } (n : ) :
            n = { re := n, im := 0 }
            @[simp]
            theorem Zsqrtd.ofInt_eq_intCast {d : } (n : ) :
            ofInt n = n
            @[simp]
            theorem Zsqrtd.nsmul_val {d : } (n : ) (x y : ) :
            n * { re := x, im := y } = { re := n * x, im := n * y }
            @[simp]
            theorem Zsqrtd.smul_val {d : } (n x y : ) :
            n * { re := x, im := y } = { re := n * x, im := n * y }
            theorem Zsqrtd.re_smul {d : } (a : ) (b : ℤ√d) :
            (a * b).re = a * b.re
            @[deprecated Zsqrtd.re_smul (since := "2025-08-31")]
            theorem Zsqrtd.smul_re {d : } (a : ) (b : ℤ√d) :
            (a * b).re = a * b.re

            Alias of Zsqrtd.re_smul.

            theorem Zsqrtd.im_smul {d : } (a : ) (b : ℤ√d) :
            (a * b).im = a * b.im
            @[deprecated Zsqrtd.im_smul (since := "2025-08-31")]
            theorem Zsqrtd.smul_im {d : } (a : ) (b : ℤ√d) :
            (a * b).im = a * b.im

            Alias of Zsqrtd.im_smul.

            @[simp]
            theorem Zsqrtd.muld_val {d : } (x y : ) :
            sqrtd * { re := x, im := y } = { re := d * y, im := x }
            @[simp]
            theorem Zsqrtd.dmuld {d : } :
            sqrtd * sqrtd = d
            @[simp]
            theorem Zsqrtd.smuld_val {d : } (n x y : ) :
            sqrtd * n * { re := x, im := y } = { re := d * n * y, im := n * x }
            theorem Zsqrtd.decompose {d x y : } :
            { re := x, im := y } = x + sqrtd * y
            theorem Zsqrtd.mul_star {d x y : } :
            { re := x, im := y } * star { re := x, im := y } = x * x - d * y * y
            theorem Zsqrtd.intCast_dvd {d : } (z : ) (a : ℤ√d) :
            z a z a.re z a.im
            @[simp]
            theorem Zsqrtd.intCast_dvd_intCast {d : } (a b : ) :
            a b a b
            theorem Zsqrtd.eq_of_smul_eq_smul_left {d a : } {b c : ℤ√d} (ha : a 0) (h : a * b = a * c) :
            b = c
            theorem Zsqrtd.gcd_eq_zero_iff {d : } (a : ℤ√d) :
            a.re.gcd a.im = 0 a = 0
            theorem Zsqrtd.gcd_pos_iff {d : } (a : ℤ√d) :
            0 < a.re.gcd a.im a 0
            theorem Zsqrtd.isCoprime_of_dvd_isCoprime {d : } {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b a) :
            theorem Zsqrtd.exists_coprime_of_gcd_pos {d : } {a : ℤ√d} (hgcd : 0 < a.re.gcd a.im) :
            ∃ (b : ℤ√d), a = (a.re.gcd a.im) * b IsCoprime b.re b.im
            def Zsqrtd.SqLe (a c b d : ) :

            Read SqLe a c b d as a √c ≤ b √d

            Equations
            Instances For
              theorem Zsqrtd.sqLe_of_le {c d x y z w : } (xz : z x) (yw : y w) (xy : SqLe x c y d) :
              SqLe z c w d
              theorem Zsqrtd.sqLe_add_mixed {c d x y z w : } (xy : SqLe x c y d) (zw : SqLe z c w d) :
              c * (x * z) d * (y * w)
              theorem Zsqrtd.sqLe_add {c d x y z w : } (xy : SqLe x c y d) (zw : SqLe z c w d) :
              SqLe (x + z) c (y + w) d
              theorem Zsqrtd.sqLe_cancel {c d x y z w : } (zw : SqLe y d x c) (h : SqLe (x + z) c (y + w) d) :
              SqLe z c w d
              theorem Zsqrtd.sqLe_smul {c d x y : } (n : ) (xy : SqLe x c y d) :
              SqLe (n * x) c (n * y) d
              theorem Zsqrtd.sqLe_mul {d x y z w : } :
              (SqLe x 1 y dSqLe z 1 w dSqLe (x * w + y * z) d (x * z + d * y * w) 1) (SqLe x 1 y dSqLe w d z 1SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (SqLe y d x 1SqLe z 1 w dSqLe (x * z + d * y * w) 1 (x * w + y * z) d) (SqLe y d x 1SqLe w d z 1SqLe (x * w + y * z) d (x * z + d * y * w) 1)
              def Zsqrtd.Nonnegg (c d : ) :
              Prop

              "Generalized" nonneg. nonnegg c d x y means a √c + b √d ≥ 0; we are interested in the case c = 1 but this is more symmetric

              Equations
              Instances For
                theorem Zsqrtd.nonnegg_comm {c d : } {x y : } :
                Nonnegg c d x y = Nonnegg d c y x
                theorem Zsqrtd.nonnegg_neg_pos {c d a b : } :
                Nonnegg c d (-a) b SqLe a d b c
                theorem Zsqrtd.nonnegg_pos_neg {c d a b : } :
                Nonnegg c d (↑a) (-b) SqLe b c a d
                theorem Zsqrtd.nonnegg_cases_right {c d a : } {b : } :
                (∀ (x : ), b = -xSqLe x c a d)Nonnegg c d (↑a) b
                theorem Zsqrtd.nonnegg_cases_left {c d b : } {a : } (h : ∀ (x : ), a = -xSqLe x d b c) :
                Nonnegg c d a b
                def Zsqrtd.norm {d : } (n : ℤ√d) :

                The norm of an element of ℤ[√d].

                Equations
                Instances For
                  theorem Zsqrtd.norm_def {d : } (n : ℤ√d) :
                  n.norm = n.re * n.re - d * n.im * n.im
                  @[simp]
                  theorem Zsqrtd.norm_zero {d : } :
                  norm 0 = 0
                  @[simp]
                  theorem Zsqrtd.norm_one {d : } :
                  norm 1 = 1
                  @[simp]
                  theorem Zsqrtd.norm_intCast {d : } (n : ) :
                  (↑n).norm = n * n
                  @[simp]
                  theorem Zsqrtd.norm_natCast {d : } (n : ) :
                  (↑n).norm = n * n
                  @[simp]
                  theorem Zsqrtd.norm_mul {d : } (n m : ℤ√d) :
                  (n * m).norm = n.norm * m.norm

                  norm as a MonoidHom.

                  Equations
                  Instances For
                    theorem Zsqrtd.norm_eq_mul_conj {d : } (n : ℤ√d) :
                    n.norm = n * star n
                    @[simp]
                    theorem Zsqrtd.norm_neg {d : } (x : ℤ√d) :
                    (-x).norm = x.norm
                    @[simp]
                    theorem Zsqrtd.norm_conj {d : } (x : ℤ√d) :
                    (star x).norm = x.norm
                    theorem Zsqrtd.norm_nonneg {d : } (hd : d 0) (n : ℤ√d) :
                    0 n.norm
                    @[simp]
                    theorem Zsqrtd.abs_norm {d : } (hd : d 0) (n : ℤ√d) :
                    theorem Zsqrtd.norm_eq_one_iff' {d : } (hd : d 0) (z : ℤ√d) :
                    theorem Zsqrtd.norm_eq_zero_iff {d : } (hd : d < 0) (z : ℤ√d) :
                    z.norm = 0 z = 0
                    theorem Zsqrtd.norm_eq_of_associated {d : } (hd : d 0) {x y : ℤ√d} (h : Associated x y) :
                    x.norm = y.norm
                    def Zsqrtd.Nonneg {d : } :
                    ℤ√dProp

                    Nonnegativity of an element of ℤ√d.

                    Equations
                    Instances For
                      instance Zsqrtd.instLECastInt {d : } :
                      LE (ℤ√d)
                      Equations
                      instance Zsqrtd.instLTCastInt {d : } :
                      LT (ℤ√d)
                      Equations
                      instance Zsqrtd.decidableNonnegg (c d : ) (a b : ) :
                      Decidable (Nonnegg c d a b)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      instance Zsqrtd.decidableNonneg {d : } (a : ℤ√d) :
                      Equations
                      Equations
                      theorem Zsqrtd.nonneg_cases {d : } {a : ℤ√d} :
                      a.Nonneg∃ (x : ) (y : ), a = { re := x, im := y } a = { re := x, im := -y } a = { re := -x, im := y }
                      theorem Zsqrtd.nonneg_add_lem {d x y z w : } (xy : { re := x, im := -y }.Nonneg) (zw : { re := -z, im := w }.Nonneg) :
                      ({ re := x, im := -y } + { re := -z, im := w }).Nonneg
                      theorem Zsqrtd.Nonneg.add {d : } {a b : ℤ√d} (ha : a.Nonneg) (hb : b.Nonneg) :
                      (a + b).Nonneg
                      theorem Zsqrtd.nonneg_iff_zero_le {d : } {a : ℤ√d} :
                      a.Nonneg 0 a
                      theorem Zsqrtd.le_of_le_le {d : } {x y z w : } (xz : x z) (yw : y w) :
                      { re := x, im := y } { re := z, im := w }
                      theorem Zsqrtd.nonneg_total {d : } (a : ℤ√d) :
                      theorem Zsqrtd.le_total {d : } (a b : ℤ√d) :
                      a b b a
                      instance Zsqrtd.preorder {d : } :
                      Equations
                      theorem Zsqrtd.le_arch {d : } (a : ℤ√d) :
                      ∃ (n : ), a n
                      theorem Zsqrtd.add_le_add_left {d : } (a b : ℤ√d) (ab : a b) (c : ℤ√d) :
                      c + a c + b
                      theorem Zsqrtd.le_of_add_le_add_left {d : } (a b c : ℤ√d) (h : c + a c + b) :
                      a b
                      theorem Zsqrtd.add_lt_add_left {d : } (a b : ℤ√d) (h : a < b) (c : ℤ√d) :
                      c + a < c + b
                      theorem Zsqrtd.nonneg_smul {d : } {a : ℤ√d} {n : } (ha : a.Nonneg) :
                      (n * a).Nonneg
                      theorem Zsqrtd.nonneg_muld {d : } {a : ℤ√d} (ha : a.Nonneg) :
                      theorem Zsqrtd.nonneg_mul_lem {d x y : } {a : ℤ√d} (ha : a.Nonneg) :
                      ({ re := x, im := y } * a).Nonneg
                      theorem Zsqrtd.nonneg_mul {d : } {a b : ℤ√d} (ha : a.Nonneg) (hb : b.Nonneg) :
                      (a * b).Nonneg
                      theorem Zsqrtd.mul_nonneg {d : } (a b : ℤ√d) :
                      0 a0 b0 a * b
                      theorem Zsqrtd.not_sqLe_succ (c d y : ) (h : 0 < c) :
                      ¬SqLe (y + 1) c 0 d

                      A nonsquare is a natural number that is not equal to the square of an integer. This is implemented as a typeclass because it's a necessary condition for much of the Pell equation theory.

                      Instances
                        @[deprecated Zsqrtd.Nonsquare.ns (since := "2025-08-28")]
                        theorem Zsqrtd.Nonsquare.ns' (x : ) [self : Nonsquare x] (n : ) :
                        x n * n

                        Alias of Zsqrtd.Nonsquare.ns.

                        theorem Zsqrtd.d_pos {d : } [dnsq : Nonsquare d] :
                        0 < d
                        theorem Zsqrtd.divides_sq_eq_zero {d : } [dnsq : Nonsquare d] {x y : } (h : x * x = d * y * y) :
                        x = 0 y = 0
                        theorem Zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : Nonsquare d] {x y : } (h : x * x = d * y * y) :
                        x = 0 y = 0
                        theorem Zsqrtd.not_divides_sq {d : } [dnsq : Nonsquare d] (x y : ) :
                        (x + 1) * (x + 1) d * (y + 1) * (y + 1)
                        theorem Zsqrtd.nonneg_antisymm {d : } [dnsq : Nonsquare d] {a : ℤ√d} :
                        a.Nonneg(-a).Nonnega = 0
                        theorem Zsqrtd.le_antisymm {d : } [dnsq : Nonsquare d] {a b : ℤ√d} (ab : a b) (ba : b a) :
                        a = b
                        instance Zsqrtd.linearOrder {d : } [dnsq : Nonsquare d] :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        theorem Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : Nonsquare d] {a b : ℤ√d} :
                        a * b = 0a = 0 b = 0
                        theorem Zsqrtd.mul_pos {d : } [dnsq : Nonsquare d] (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) :
                        0 < a * b
                        theorem Zsqrtd.norm_eq_zero {d : } (h_nonsquare : ∀ (n : ), d n * n) (a : ℤ√d) :
                        a.norm = 0 a = 0
                        theorem Zsqrtd.hom_ext {R : Type} [NonAssocRing R] {d : } (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) :
                        f = g
                        theorem Zsqrtd.hom_ext_iff {R : Type} [NonAssocRing R] {d : } {f g : ℤ√d →+* R} :
                        f = g f sqrtd = g sqrtd
                        def Zsqrtd.lift {R : Type} [CommRing R] {d : } :
                        { r : R // r * r = d } (ℤ√d →+* R)

                        The unique RingHom from ℤ√d to a ring R, constructed by replacing √d with the provided root. Conversely, this associates to every mapping ℤ√d →+* R a value of √d in R.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem Zsqrtd.lift_symm_apply_coe {R : Type} [CommRing R] {d : } (f : ℤ√d →+* R) :
                          (lift.symm f) = f sqrtd
                          @[simp]
                          theorem Zsqrtd.lift_apply_apply {R : Type} [CommRing R] {d : } (r : { r : R // r * r = d }) (a : ℤ√d) :
                          (lift r) a = a.re + a.im * r
                          theorem Zsqrtd.lift_injective {R : Type} [CommRing R] [CharZero R] {d : } (r : { r : R // r * r = d }) (hd : ∀ (n : ), d n * n) :

                          lift r is injective if d is non-square, and R has characteristic zero (that is, the map from into R is injective).

                          An element of ℤ√d has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

                          The kernel of the norm map on ℤ√d equals the submonoid of unitary elements.