Commit 2026-02-07 16:19 845a0b9a

View on Github →

feat(RingTheory/DedekindDomain/AdicValuation): unit lemmas for adicCompletionIntegers (#34918)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one