Documentation
Atlas
.
AlgebraNotes
.
code
.
QuadraticFields
Search
return to top
source
Imports
Init
Mathlib.RingTheory.AdjoinRoot
Mathlib.GroupTheory.SpecificGroups.Cyclic
Mathlib.NumberTheory.NumberField.ClassNumber
Mathlib.RingTheory.DedekindDomain.PID
Imported by
instFactIrreducibleXSqPlusFive
QSqrtNeg5
classNumber_QSqrtNeg5
classGroup_QSqrtNeg5_iso
source
instance
instFactIrreducibleXSqPlusFive
:
Fact
(
Irreducible
(
Polynomial.X
^
2
+
Polynomial.C
5
))
source
@[reducible, inline]
noncomputable abbrev
QSqrtNeg5
:
Type
Instances For
source
theorem
classNumber_QSqrtNeg5
:
NumberField.classNumber
QSqrtNeg5
=
2
source
theorem
classGroup_QSqrtNeg5_iso
:
Nonempty
(
ClassGroup
(
NumberField.RingOfIntegers
QSqrtNeg5
)
≃*
Multiplicative
(
ZMod
2
)
)