Def IsDedekindDomain.FiniteAdeleRing

Modification history

2025-12-01 21:12
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
chore: make FiniteAdeleRing a def rather than an abbrev (#32277) …
Added IsDedekindDomain.FiniteAdeleRingView on Github →