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 #

number_field.class_number: the class number of a number field is the (finite) cardinality of the class group of its ring of integers

source

@[protected, instance]

noncomputable def number_field.ring_of_integers.class_group.fintype (K : Type u_1) [field K] [number_field K] :

fintype (class_group ↥(number_field.ring_of_integers K))

Equations

number_field.ring_of_integers.class_group.fintype K = class_group.fintype_of_admissible_of_finite ℚ K absolute_value.abs_is_admissible

source

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

number_field.class_number K = fintype.card (class_group ↥(number_field.ring_of_integers K))

source

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

number_field.class_number K = 1 ↔ is_principal_ideal_ring ↥(number_field.ring_of_integers K)

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

source

theorem rat.class_number_eq :

number_field.class_number ℚ = 1