Theorem IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff

Modification history

2026-01-03 19:24

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

feat(RingTheory/DedekindDomain/AdicValuation): introduce `intAdicAbv` (#33324) …

Modified IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff View on Github →

2025-06-03 07:59

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

feat(RingTheory/DedekindDomain/AdicValuation): Generalize APIs for `adicAbv` (#25330) …

Added IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff View on Github →