NumberField.classNumber_eq_one_iff

theorem NumberField.classNumber_eq_one_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NumberField.classNumber K = 1 ↔ IsPrincipalIdealRing ↥(NumberField.ringOfIntegers K)

The theorem states that for any number field `K`, the class number of `K` is `1` if and only if the ring of integers in `K` is a Principal Ideal Ring (PID). To be more precise, the class number of a number field is the cardinality of its class group - the set of equivalence classes of ideals (finite in number). A number field has a class number of `1` if all of its ideals can be generated by a single element, i.e., if its ring of integers is a PID.

More concisely: A number field `K` has class number 1 if and only if its ring of integers is a principal ideal ring.