Theorem IsDedekindDomain.FiniteAdeleRing.algebraMap_apply

Modification history

2026-05-21 08:00
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: unit lemmas and embedding for `FiniteAdeleRing` (#35820)
Added IsDedekindDomain.FiniteAdeleRing.algebraMap_applyView on Github →