Commit 2023-06-24 18:53 fab65d80

View on Github →

feat: port NumberTheory.NumberField.ClassNumber (#5456)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/ClassNumber.lean

added theorem NumberField.classNumber_eq_one_iff

added theorem Rat.classNumber_eq