mk — Mathlib · SciLib

English

The mk constructor sends an element a ∈ M to its Archimedean class mk a in MulArchimedeanClass M; mk is constant on Archimedean-equivalent elements.

Русский

Конструктор mk отправляет элемент a ∈ M в его Архимедов класс mk a в MulArchimedeanClass M; mk константен на элементы, эквивалентные по Архимедову отношению.

LaTeX

$$$mk : M \to MulArchimedeanClass M$$$

Lean4

/-- The archimedean class of a given element. -/
@[to_additive /-- The archimedean class of a given element. -/
    ]
def mk (a : M) : MulArchimedeanClass M :=
  toAntisymmetrization _ (MulArchimedeanOrder.of a)

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