Commit 2026-05-21 08:00 0f331496

View on Github →

feat: unit lemmas and embedding for FiniteAdeleRing (#35820)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

added theorem IsDedekindDomain.FiniteAdeleRing.algebraMap_apply

added theorem IsDedekindDomain.FiniteAdeleRing.infinite_valued_ne_one_of_not_isUnit

added theorem IsDedekindDomain.FiniteAdeleRing.isUnit_iff

added def IsDedekindDomain.FiniteAdeleRing.unitEmbedding

added theorem IsDedekindDomain.FiniteAdeleRing.unitEmbedding_apply

added theorem IsDedekindDomain.FiniteAdeleRing.unitsEquiv_finite_valued_eq_one