Def IsDedekindDomain.HeightOneSpectrum.Support

Modification history

2025-04-23 09:49

Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles (#23542) …

Added IsDedekindDomain.HeightOneSpectrum.Support View on Github →