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
The class number of a number field is the (finite) cardinality of the class group.
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 (RingOfIntegers K))
: