# mathlibdocumentation

number_theory.class_number.number_field

# 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 #

• number_field.class_number: the class number of a number field is the (finite) cardinality of the class group of its ring of integers
@[protected, instance]
noncomputable def number_field.ring_of_integers.class_group.fintype (K : Type u_1) [field K] [number_field K] :
Equations
noncomputable def number_field.class_number (K : Type u_1) [field K] [number_field K] :

The class number of a number field is the (finite) cardinality of the class group.

Equations
theorem number_field.class_number_eq_one_iff {K : Type u_1} [field K] [number_field K] :

The class number of a number field is 1 iff the ring of integers is a PID.