Theorem IsDedekindDomain.FiniteAdeleRing.unitEmbedding_apply

Modification history

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