Commit 2023-01-30 13:16 ce690641

View on Github →

feat: port NumberTheory.ClassNumber.AdmissibleAbsoluteValue (#1941)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean

added theorem AbsoluteValue.IsAdmissible.exists_approx

added theorem AbsoluteValue.IsAdmissible.exists_approx_aux

added theorem AbsoluteValue.IsAdmissible.exists_partition

added structure AbsoluteValue.IsAdmissible