mathlib3 documentation


The ideal class group #

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

This file defines the ideal class group class_group R of fractional ideals of R inside its field of fractions.

Main definitions #

Main results #

Implementation details #

The definition of class_group R involves fraction_ring R. However, the API should be completely identical no matter the choice of field of fractions for R.


to_principal_ideal R K x sends x ≠ 0 : K to the fractional R-ideal generated by x

@[protected, instance]
def class_group (R : Type u_1) [comm_ring R] [is_domain R] :
Type u_1

The ideal class group of R is the group of invertible fractional ideals modulo the principal ideals.

Instances for class_group
@[protected, instance]
noncomputable def class_group.comm_group (R : Type u_1) [comm_ring R] [is_domain R] :
@[protected, instance]
noncomputable def class_group.inhabited (R : Type u_1) [comm_ring R] [is_domain R] :
noncomputable def {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] :

Send a nonzero fractional ideal to the corresponding class in the class group.

theorem class_group.mk_eq_mk_of_coe_ideal {R : Type u_1} [comm_ring R] [is_domain R] {I J : (fractional_ideal (non_zero_divisors R) (fraction_ring R))ˣ} {I' J' : ideal R} (hI : I = I') (hJ : J = J') :
theorem class_group.induction {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] {P : class_group R Prop} (h : (I : (fractional_ideal (non_zero_divisors R) K)ˣ), P ( I)) (x : class_group R) :
P x

Induction principle for the class group: to show something holds for all x : class_group R, we can choose a fraction field K and show it holds for the equivalence class of each I : fractional_ideal R⁰ K.

The definition of the class group does not depend on the choice of field of fractions.


Send a nonzero integral ideal to an invertible fractional ideal.


Send a nonzero ideal to the corresponding class in the class group.

@[protected, instance]
noncomputable def class_group.fintype {R : Type u_1} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] :

The class group of principal ideal domain is finite (in fact a singleton).

See class_group.fintype_of_admissible for a finiteness proof that works for rings of integers of global fields.


The class number of a principal ideal domain is 1.

The class number is 1 iff the ring of integers is a principal ideal domain.