mathlib3 documentation

number_theory.class_number.function_field

Class numbers of function 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 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 #

noncomputable def function_field.class_number (Fq F : Type) [field Fq] [fintype Fq] [field F] [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F] [is_scalar_tower (polynomial Fq) (ratfunc Fq) F] [function_field Fq F] [is_separable (ratfunc Fq) F] :

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

Equations

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