Theorem IsDedekindDomain.HeightOneSpectrum.Support.finite

Modification history

2025-04-23 09:49
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles (#23542) …
Added IsDedekindDomain.HeightOneSpectrum.Support.finiteView on Github →