integerSetToAssociates — Mathlib

English

There is a canonical map integerSetK → Associates((𝓞K)⁰) sending an element a ∈ integerSet(K) to the associate class of its preimage in the ring of integers.

Русский

Существует каноническое отображение из integerSet(K) в Assciates((𝓞K)⁰), отправляющее a в ассоциированное класс предобраза в кольце целых чисел.

LaTeX

$$$\\operatorname{integerSetToAssociates}(a) = \\llbracket \\operatorname{preimageOfMemIntegerSet}(a) \\rrbracket.$$$

Lean4

/-- The map that sends an element of `a : integerSet K` to the associates class
of its preimage in `(𝓞 K)⁰`. By quotienting by the kernel of the map, which is equal to the
subgroup of torsion, we get the equivalence `integerSetQuotEquivAssociates`. -/
def integerSetToAssociates (a : integerSet K) : Associates (𝓞 K)⁰ :=
  ⟦preimageOfMemIntegerSet a⟧

Похожие утверждения