15.6. The class group🔗

The class group measures the failure of 𝓞 K to be a principal ideal domain. In Lean this is ClassGroup (𝓞 K):

ClassGroup (𝓞 K) : Type u_1#check (ClassGroup (𝓞 K) : Type _)

For a number field the class group is finite, this is one of the central finiteness theorems of the subject, available as an instance:

example : Finite (ClassGroup (𝓞 K)) := inferInstance

Its cardinality is the class number NumberField.classNumber, which is defined as this cardinality:

example :
    classNumber K = Fintype.card (ClassGroup (𝓞 K)) := rfl

To produce elements of the class group from ideals, use ClassGroup.mk0, which sends a nonzero ideal to its class.