Def NumberField.IdeleGroup.unitEmbedding

Modification history

2026-08-27 17:33

Mathlib/NumberTheory/NumberField/AdeleRing.lean

feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735) …

Added NumberField.IdeleGroup.unitEmbedding View on Github →