Mathlib Changelog
v4
Changelog
About
Github
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 →