mathlib3 documentation

number_theory.number_field.class_number

Class numbers of number fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.