# mathlibdocumentation

number_theory.class_number.function_field

# Class numbers of function fields #

This file defines the class number of a function 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 #

• function_field.class_number: the class number of a function field is the (finite) cardinality of the class group of its ring of integers
@[protected, instance]
noncomputable def function_field.ring_of_integers.class_group.fintype (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [ (ratfunc Fq) F] [ F] [is_separable (ratfunc Fq) F] :
Equations
noncomputable def function_field.class_number (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [ (ratfunc Fq) F] [ F] [is_separable (ratfunc Fq) F] :

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

Equations
theorem function_field.class_number_eq_one_iff (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [ (ratfunc Fq) F] [ F] [is_separable (ratfunc Fq) F] :

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