Theorem IsDedekindDomain.FiniteAdeleRing.infinite_valued_ne_one_of_not_isUnit

Modification history

2026-07-29 08:07
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: notation for adele rings (#40535) …
Modified IsDedekindDomain.FiniteAdeleRing.infinite_valued_ne_one_of_not_isUnitView on Github →
2026-05-21 08:00
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: unit lemmas and embedding for `FiniteAdeleRing` (#35820)
Added IsDedekindDomain.FiniteAdeleRing.infinite_valued_ne_one_of_not_isUnitView on Github →