instance instFactIrreducibleXSqPlusFive : Fact (Irreducible (Polynomial.X ^ 2 + Polynomial.C 5))

@[reducible, inline]

noncomputable abbrev QSqrtNeg5 : Type

theorem classNumber_QSqrtNeg5 : NumberField.classNumber QSqrtNeg5 = 2

theorem classGroup_QSqrtNeg5_iso : Nonempty (ClassGroup (NumberField.RingOfIntegers QSqrtNeg5) ≃* Multiplicative (ZMod 2))