Commit 2025-02-17 19:20 093803ad

View on Github →

feat: injectivity of algebraMap for FiniteIntegralAdeles to FiniteAdeleRing (#21163)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

added theorem DedekindDomain.FiniteAdeleRing.coe_algebraMap'