ℤ[√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
.
Equations
- instDecidableEqZsqrtd = decEqZsqrtd✝
Equations
- «termℤ√_» = Lean.ParserDescr.node `termℤ√_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℤ√") (Lean.ParserDescr.cat `term 100))
Instances For
The zero of the ring
Equations
- Zsqrtd.instZero = { zero := Zsqrtd.ofInt 0 }
The one of the ring
Equations
- Zsqrtd.instOne = { one := Zsqrtd.ofInt 1 }
Equations
- Zsqrtd.addCommGroup = AddCommGroup.mk ⋯
Equations
- Zsqrtd.addGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Zsqrtd.instCommMonoid = inferInstance
Equations
- Zsqrtd.instCommSemigroup = inferInstance
Equations
- Zsqrtd.instAddCommSemigroup = inferInstance
Equations
- Zsqrtd.instAddSemigroup = inferInstance
Equations
- Zsqrtd.instCommSemiring = inferInstance
Equations
- Zsqrtd.instStarRing = StarRing.mk ⋯
Alias of Zsqrtd.natCast_re
.
Alias of Zsqrtd.natCast_im
.
Alias of Zsqrtd.natCast_val
.
Alias of Zsqrtd.intCast_re
.
Alias of Zsqrtd.intCast_im
.
Alias of Zsqrtd.intCast_val
.
Alias of Zsqrtd.ofInt_eq_intCast
.
Alias of Int.cast_add
.
Alias of Int.cast_sub
.
Alias of Int.cast_mul
.
Alias of Int.cast_inj
.
Alias of Zsqrtd.intCast_dvd_intCast
.
"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
- Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.ofNat b) = True
- Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.negSucc b) = Zsqrtd.SqLe (b + 1) c a d
- Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.ofNat b) = Zsqrtd.SqLe (a + 1) d b c
- Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = False
Instances For
Alias of Zsqrtd.norm_intCast
.
Alias of Zsqrtd.norm_natCast
.
Nonnegativity of an element of ℤ√d
.
Equations
- { re := a, im := b }.Nonneg = Zsqrtd.Nonnegg d 1 a b
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- { re := a, im := b }.decidableNonneg = Zsqrtd.decidableNonnegg d 1 a b
Equations
- Zsqrtd.linearOrder = LinearOrder.mk ⋯ Zsqrtd.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- Zsqrtd.instLinearOrderedCommRingCastInt = LinearOrderedCommRing.mk ⋯
Equations
- Zsqrtd.instLinearOrderedRingCastInt = inferInstance
Equations
- Zsqrtd.instOrderedRingCastInt = inferInstance
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
The kernel of the norm map on ℤ√d
equals the submonoid of unitary elements.