out — Mathlib

English

The representative function out selects a representative element from each archimedean class.

Русский

Функция out выбирает представителя из каждого архимедова класса.

LaTeX

$$$out: MulArchimedeanClass M \to M$$$

Lean4

/-- Choose a representative element from a given archimedean class. -/
@[to_additive /-- Choose a representative element from a given archimedean class. -/
    ]
noncomputable def out (A : MulArchimedeanClass M) : M :=
  (Quotient.out A).val

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