mathlib documentation

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 #

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

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