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.instFintypeClassGroupSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingIsDomainToIsDomainIsDedekindDomainIsDomainTo_principal_ideal_domain
(K : Type u_1)
[Field K]
[NumberField K]
:
Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })
The class number of a number field is the (finite) cardinality of the class group.
Instances For
theorem
NumberField.classNumber_eq_one_iff
{K : Type u_1}
[Field K]
[NumberField K]
:
NumberField.classNumber K = 1 ↔ IsPrincipalIdealRing { x // x ∈ NumberField.ringOfIntegers K }
The class number of a number field is 1 iff the ring of integers is a PID.