Def DedekindDomain.FiniteAdeleRing

Modification history

2024-06-26 12:43
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: the finite adele ring is an algebra over the finite integral adeles. (#13705)
Modified DedekindDomain.FiniteAdeleRingView on Github →
2024-05-28 11:04
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: add API for finite adele rings (#13021) …
Added DedekindDomain.FiniteAdeleRingView on Github →