Class numbers of number fields #
This file defines the class number of a number field as the (finite) cardinality of the class group of its ring of integers. It also proves some elementary results on the class number.
Main definitions #
NumberField.classNumber: the class number of a number field is the (finite) cardinality of the class group of its ring of integers
noncomputable instance
NumberField.RingOfIntegers.instFintypeClassGroup
(K : Type u_1)
[Field K]
[NumberField K]
:
The class number of a number field is the (finite) cardinality of the class group.
Equations
Instances For
The class number of a number field is 1 iff the ring of integers is a PID.
theorem
NumberField.exists_ideal_in_class_of_norm_le
{K : Type u_1}
[Field K]
[NumberField K]
(C : ClassGroup ↥(NumberField.ringOfIntegers K))
:
∃ (I : ↥(nonZeroDivisors (Ideal ↥(NumberField.ringOfIntegers K)))),
ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.NrComplexPlaces K * (↑(Nat.factorial (FiniteDimensional.finrank ℚ K)) / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * Real.sqrt |↑(NumberField.discr K)|)
theorem
RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
{K : Type u_1}
[Field K]
[NumberField K]
(h : ↑|NumberField.discr K| < (2 * (Real.pi / 4) ^ NumberField.InfinitePlace.NrComplexPlaces K * (↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K / ↑(Nat.factorial (FiniteDimensional.finrank ℚ K)))) ^ 2)
: