Def IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef

Modification history

2026-01-03 19:24

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

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

Added IsDedekindDomain.HeightOneSpectrum.intAdicAbvDef View on Github →