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.

Instances For
    theorem Zsqrtd.ext {d : } {x y : ℤ√d} (re : x.re = y.re) (im : x.im = y.im) :
    x = y
    instance instDecidableEqZsqrtd {d✝ : } :
    Equations
    • instDecidableEqZsqrtd = decEqZsqrtd✝
    def Zsqrtd.ofInt {d : } (n : ) :

    Convert an integer to a ℤ√d

    Equations
    Instances For
      theorem Zsqrtd.ofInt_re {d : } (n : ) :
      (Zsqrtd.ofInt n).re = n
      theorem Zsqrtd.ofInt_im {d : } (n : ) :
      (Zsqrtd.ofInt n).im = 0
      instance Zsqrtd.instZero {d : } :

      The zero of the ring

      Equations
      @[simp]
      theorem Zsqrtd.zero_re {d : } :
      @[simp]
      theorem Zsqrtd.zero_im {d : } :
      Equations
      • Zsqrtd.instInhabited = { default := 0 }
      instance Zsqrtd.instOne {d : } :

      The one of the ring

      Equations
      @[simp]
      theorem Zsqrtd.one_re {d : } :
      @[simp]
      theorem Zsqrtd.one_im {d : } :
      def Zsqrtd.sqrtd {d : } :

      The representative of √d in the ring

      Equations
      • Zsqrtd.sqrtd = { re := 0, im := 1 }
      Instances For
        @[simp]
        theorem Zsqrtd.sqrtd_re {d : } :
        Zsqrtd.sqrtd.re = 0
        @[simp]
        theorem Zsqrtd.sqrtd_im {d : } :
        Zsqrtd.sqrtd.im = 1
        instance Zsqrtd.instAdd {d : } :

        Addition of elements of ℤ√d

        Equations
        • Zsqrtd.instAdd = { add := fun (z w : ℤ√d) => { re := z.re + w.re, im := z.im + w.im } }
        @[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.add_re {d : } (z w : ℤ√d) :
        (z + w).re = z.re + w.re
        @[simp]
        theorem Zsqrtd.add_im {d : } (z w : ℤ√d) :
        (z + w).im = z.im + w.im
        instance Zsqrtd.instNeg {d : } :

        Negation in ℤ√d

        Equations
        • Zsqrtd.instNeg = { neg := fun (z : ℤ√d) => { re := -z.re, im := -z.im } }
        @[simp]
        theorem Zsqrtd.neg_re {d : } (z : ℤ√d) :
        (-z).re = -z.re
        @[simp]
        theorem Zsqrtd.neg_im {d : } (z : ℤ√d) :
        (-z).im = -z.im
        instance Zsqrtd.instMul {d : } :

        Multiplication in ℤ√d

        Equations
        • Zsqrtd.instMul = { mul := fun (z w : ℤ√d) => { re := z.re * w.re + d * z.im * w.im, im := z.re * w.im + z.im * w.re } }
        @[simp]
        theorem Zsqrtd.mul_re {d : } (z w : ℤ√d) :
        (z * w).re = z.re * w.re + d * z.im * w.im
        @[simp]
        theorem Zsqrtd.mul_im {d : } (z w : ℤ√d) :
        (z * w).im = z.re * w.im + z.im * w.re
        Equations
        @[simp]
        theorem Zsqrtd.sub_re {d : } (z w : ℤ√d) :
        (z - w).re = z.re - w.re
        @[simp]
        theorem Zsqrtd.sub_im {d : } (z w : ℤ√d) :
        (z - w).im = z.im - w.im
        Equations
        instance Zsqrtd.commRing {d : } :
        Equations
        Equations
        • Zsqrtd.instAddMonoid = inferInstance
        instance Zsqrtd.instMonoid {d : } :
        Equations
        • Zsqrtd.instMonoid = inferInstance
        Equations
        • Zsqrtd.instCommMonoid = inferInstance
        Equations
        • Zsqrtd.instCommSemigroup = inferInstance
        Equations
        • Zsqrtd.instSemigroup = inferInstance
        Equations
        • Zsqrtd.instAddCommSemigroup = inferInstance
        Equations
        • Zsqrtd.instAddSemigroup = inferInstance
        Equations
        • Zsqrtd.instCommSemiring = inferInstance
        Equations
        • Zsqrtd.instSemiring = inferInstance
        instance Zsqrtd.instRing {d : } :
        Equations
        • Zsqrtd.instRing = inferInstance
        Equations
        • Zsqrtd.instDistrib = inferInstance
        instance Zsqrtd.instStar {d : } :

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

        Equations
        • Zsqrtd.instStar = { star := fun (z : ℤ√d) => { re := z.re, im := -z.im } }
        @[simp]
        theorem Zsqrtd.star_mk {d : } (x y : ) :
        star { re := x, im := y } = { re := x, im := -y }
        @[simp]
        theorem Zsqrtd.star_re {d : } (z : ℤ√d) :
        (star z).re = z.re
        @[simp]
        theorem Zsqrtd.star_im {d : } (z : ℤ√d) :
        (star z).im = -z.im
        Equations
        @[simp]
        theorem Zsqrtd.natCast_re {d : } (n : ) :
        (↑n).re = n
        @[simp]
        theorem Zsqrtd.ofNat_re {d : } (n : ) [n.AtLeastTwo] :
        (OfNat.ofNat n).re = n
        @[simp]
        theorem Zsqrtd.natCast_im {d : } (n : ) :
        (↑n).im = 0
        @[simp]
        theorem Zsqrtd.ofNat_im {d : } (n : ) [n.AtLeastTwo] :
        (OfNat.ofNat n).im = 0
        theorem Zsqrtd.natCast_val {d : } (n : ) :
        n = { re := n, im := 0 }
        @[simp]
        theorem Zsqrtd.intCast_re {d : } (n : ) :
        (↑n).re = n
        @[simp]
        theorem Zsqrtd.intCast_im {d : } (n : ) :
        (↑n).im = 0
        theorem Zsqrtd.intCast_val {d : } (n : ) :
        n = { re := n, im := 0 }
        @[simp]
        theorem Zsqrtd.ofInt_eq_intCast {d : } (n : ) :
        @[deprecated Zsqrtd.natCast_re]
        theorem Zsqrtd.coe_nat_re {d : } (n : ) :
        (↑n).re = n

        Alias of Zsqrtd.natCast_re.

        @[deprecated Zsqrtd.natCast_im]
        theorem Zsqrtd.coe_nat_im {d : } (n : ) :
        (↑n).im = 0

        Alias of Zsqrtd.natCast_im.

        @[deprecated Zsqrtd.natCast_val]
        theorem Zsqrtd.coe_nat_val {d : } (n : ) :
        n = { re := n, im := 0 }

        Alias of Zsqrtd.natCast_val.

        @[deprecated Zsqrtd.intCast_re]
        theorem Zsqrtd.coe_int_re {d : } (n : ) :
        (↑n).re = n

        Alias of Zsqrtd.intCast_re.

        @[deprecated Zsqrtd.intCast_im]
        theorem Zsqrtd.coe_int_im {d : } (n : ) :
        (↑n).im = 0

        Alias of Zsqrtd.intCast_im.

        @[deprecated Zsqrtd.intCast_val]
        theorem Zsqrtd.coe_int_val {d : } (n : ) :
        n = { re := n, im := 0 }

        Alias of Zsqrtd.intCast_val.

        @[deprecated Zsqrtd.ofInt_eq_intCast]
        theorem Zsqrtd.ofInt_eq_coe {d : } (n : ) :

        Alias of Zsqrtd.ofInt_eq_intCast.

        @[simp]
        theorem Zsqrtd.smul_val {d : } (n x y : ) :
        n * { re := x, im := y } = { re := n * x, im := n * y }
        theorem Zsqrtd.smul_re {d : } (a : ) (b : ℤ√d) :
        (a * b).re = a * b.re
        theorem Zsqrtd.smul_im {d : } (a : ) (b : ℤ√d) :
        (a * b).im = a * b.im
        @[simp]
        theorem Zsqrtd.muld_val {d : } (x y : ) :
        Zsqrtd.sqrtd * { re := x, im := y } = { re := d * y, im := x }
        @[simp]
        theorem Zsqrtd.dmuld {d : } :
        Zsqrtd.sqrtd * Zsqrtd.sqrtd = d
        @[simp]
        theorem Zsqrtd.smuld_val {d : } (n x y : ) :
        Zsqrtd.sqrtd * n * { re := x, im := y } = { re := d * n * y, im := n * x }
        theorem Zsqrtd.decompose {d x y : } :
        { re := x, im := y } = x + Zsqrtd.sqrtd * y
        theorem Zsqrtd.mul_star {d x y : } :
        { re := x, im := y } * star { re := x, im := y } = x * x - d * y * y
        @[deprecated Int.cast_add]
        theorem Zsqrtd.coe_int_add {R : Type u} [AddGroupWithOne R] (m n : ) :
        (m + n) = m + n

        Alias of Int.cast_add.

        @[deprecated Int.cast_sub]
        theorem Zsqrtd.coe_int_sub {R : Type u} [AddGroupWithOne R] (m n : ) :
        (m - n) = m - n

        Alias of Int.cast_sub.

        @[deprecated Int.cast_mul]
        theorem Zsqrtd.coe_int_mul {α : Type u_1} [NonAssocRing α] (m n : ) :
        (m * n) = m * n

        Alias of Int.cast_mul.

        @[deprecated Int.cast_inj]
        theorem Zsqrtd.coe_int_inj {α : Type u_3} [AddGroupWithOne α] [CharZero α] {m n : } :
        m = n m = n

        Alias of Int.cast_inj.

        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
        @[deprecated Zsqrtd.intCast_dvd]
        theorem Zsqrtd.coe_int_dvd_iff {d : } (z : ) (a : ℤ√d) :
        z a z a.re z a.im

        Alias of Zsqrtd.intCast_dvd.

        @[deprecated Zsqrtd.intCast_dvd_intCast]
        theorem Zsqrtd.coe_int_dvd_coe_int {d : } (a b : ) :
        a b a b

        Alias of Zsqrtd.intCast_dvd_intCast.

        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.coprime_of_dvd_coprime {d : } {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b a) :
        IsCoprime b.re b.im
        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 : Zsqrtd.SqLe x c y d) :
          Zsqrtd.SqLe z c w d
          theorem Zsqrtd.sqLe_add_mixed {c d x y z w : } (xy : Zsqrtd.SqLe x c y d) (zw : Zsqrtd.SqLe z c w d) :
          c * (x * z) d * (y * w)
          theorem Zsqrtd.sqLe_add {c d x y z w : } (xy : Zsqrtd.SqLe x c y d) (zw : Zsqrtd.SqLe z c w d) :
          Zsqrtd.SqLe (x + z) c (y + w) d
          theorem Zsqrtd.sqLe_cancel {c d x y z w : } (zw : Zsqrtd.SqLe y d x c) (h : Zsqrtd.SqLe (x + z) c (y + w) d) :
          Zsqrtd.SqLe z c w d
          theorem Zsqrtd.sqLe_smul {c d x y : } (n : ) (xy : Zsqrtd.SqLe x c y d) :
          Zsqrtd.SqLe (n * x) c (n * y) d
          theorem Zsqrtd.sqLe_mul {d x y z w : } :
          (Zsqrtd.SqLe x 1 y dZsqrtd.SqLe z 1 w dZsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1) (Zsqrtd.SqLe x 1 y dZsqrtd.SqLe w d z 1Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (Zsqrtd.SqLe y d x 1Zsqrtd.SqLe z 1 w dZsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (Zsqrtd.SqLe y d x 1Zsqrtd.SqLe w d z 1Zsqrtd.SqLe (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 : } :
            theorem Zsqrtd.nonnegg_neg_pos {c d a b : } :
            Zsqrtd.Nonnegg c d (-a) b Zsqrtd.SqLe a d b c
            theorem Zsqrtd.nonnegg_pos_neg {c d a b : } :
            Zsqrtd.Nonnegg c d (↑a) (-b) Zsqrtd.SqLe b c a d
            theorem Zsqrtd.nonnegg_cases_right {c d a : } {b : } :
            (∀ (x : ), b = -xZsqrtd.SqLe x c a d)Zsqrtd.Nonnegg c d (↑a) b
            theorem Zsqrtd.nonnegg_cases_left {c d b : } {a : } (h : ∀ (x : ), a = -xZsqrtd.SqLe x d b c) :
            Zsqrtd.Nonnegg c d a b
            def Zsqrtd.norm {d : } (n : ℤ√d) :

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

            Equations
            • n.norm = n.re * n.re - d * n.im * n.im
            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 : } :
              @[simp]
              theorem Zsqrtd.norm_one {d : } :
              @[simp]
              theorem Zsqrtd.norm_intCast {d : } (n : ) :
              (↑n).norm = n * n
              @[deprecated Zsqrtd.norm_intCast]
              theorem Zsqrtd.norm_int_cast {d : } (n : ) :
              (↑n).norm = n * n

              Alias of Zsqrtd.norm_intCast.

              @[simp]
              theorem Zsqrtd.norm_natCast {d : } (n : ) :
              (↑n).norm = n * n
              @[deprecated Zsqrtd.norm_natCast]
              theorem Zsqrtd.norm_nat_cast {d : } (n : ) :
              (↑n).norm = n * n

              Alias of Zsqrtd.norm_natCast.

              @[simp]
              theorem Zsqrtd.norm_mul {d : } (n m : ℤ√d) :
              (n * m).norm = n.norm * m.norm

              norm as a MonoidHom.

              Equations
              • Zsqrtd.normMonoidHom = { toFun := Zsqrtd.norm, map_one' := , map_mul' := }
              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
                theorem Zsqrtd.norm_eq_one_iff {d : } {x : ℤ√d} :
                x.norm.natAbs = 1 IsUnit x
                theorem Zsqrtd.norm_eq_one_iff' {d : } (hd : d 0) (z : ℤ√d) :
                z.norm = 1 IsUnit z
                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
                  • Zsqrtd.instLECastInt = { le := fun (a b : ℤ√d) => (b - a).Nonneg }
                  instance Zsqrtd.instLTCastInt {d : } :
                  LT (ℤ√d)
                  Equations
                  • Zsqrtd.instLTCastInt = { lt := fun (a b : ℤ√d) => ¬b a }
                  instance Zsqrtd.decidableNonnegg (c d : ) (a b : ) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance Zsqrtd.decidableNonneg {d : } (a : ℤ√d) :
                  Decidable a.Nonneg
                  Equations
                  instance Zsqrtd.decidableLE {d : } :
                  DecidableRel fun (x1 x2 : ℤ√d) => x1 x2
                  Equations
                  • x✝.decidableLE x = (x - x✝).decidableNonneg
                  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) :
                  a.Nonneg (-a).Nonneg
                  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) :
                  (Zsqrtd.sqrtd * 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) :
                  ¬Zsqrtd.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
                    theorem Zsqrtd.Nonsquare.ns (x : ) [Zsqrtd.Nonsquare x] (n : ) :
                    x n * n
                    theorem Zsqrtd.d_pos {d : } [dnsq : Zsqrtd.Nonsquare d] :
                    0 < d
                    theorem Zsqrtd.divides_sq_eq_zero {d : } [dnsq : Zsqrtd.Nonsquare d] {x y : } (h : x * x = d * y * y) :
                    x = 0 y = 0
                    theorem Zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : Zsqrtd.Nonsquare d] {x y : } (h : x * x = d * y * y) :
                    x = 0 y = 0
                    theorem Zsqrtd.not_divides_sq {d : } [dnsq : Zsqrtd.Nonsquare d] (x y : ) :
                    (x + 1) * (x + 1) d * (y + 1) * (y + 1)
                    theorem Zsqrtd.nonneg_antisymm {d : } [dnsq : Zsqrtd.Nonsquare d] {a : ℤ√d} :
                    a.Nonneg(-a).Nonnega = 0
                    theorem Zsqrtd.le_antisymm {d : } [dnsq : Zsqrtd.Nonsquare d] {a b : ℤ√d} (ab : a b) (ba : b a) :
                    a = b
                    instance Zsqrtd.linearOrder {d : } [dnsq : Zsqrtd.Nonsquare d] :
                    Equations
                    • Zsqrtd.linearOrder = LinearOrder.mk Zsqrtd.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE
                    theorem Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : Zsqrtd.Nonsquare d] {a b : ℤ√d} :
                    a * b = 0a = 0 b = 0
                    theorem Zsqrtd.mul_pos {d : } [dnsq : Zsqrtd.Nonsquare d] (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) :
                    0 < a * b
                    Equations
                    Equations
                    • Zsqrtd.instLinearOrderedRingCastInt = inferInstance
                    Equations
                    • Zsqrtd.instOrderedRingCastInt = inferInstance
                    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} [Ring R] {d : } (f g : ℤ√d →+* R) (h : f Zsqrtd.sqrtd = g Zsqrtd.sqrtd) :
                    f = g
                    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) :
                      (Zsqrtd.lift.symm f) = f Zsqrtd.sqrtd
                      @[simp]
                      theorem Zsqrtd.lift_apply_apply {R : Type} [CommRing R] {d : } (r : { r : R // r * r = d }) (a : ℤ√d) :
                      (Zsqrtd.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) :
                      Function.Injective (Zsqrtd.lift r)

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

                      theorem Zsqrtd.norm_eq_one_iff_mem_unitary {d : } {a : ℤ√d} :
                      a.norm = 1 a unitary (ℤ√d)

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

                      theorem Zsqrtd.mker_norm_eq_unitary {d : } :
                      MonoidHom.mker Zsqrtd.normMonoidHom = unitary (ℤ√d)

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