addValuation — Mathlib

English

There exists an AddValuation on ArchimedeanClass R given by the map x ↦ mk x.

Русский

Существует оценка по добавлению на ArchimedeanClass R, задаваемая отображением x ↦ mk x.

LaTeX

$$$$ \text{AddValuation on } R \text{ given by } v(x) = \operatorname{mk}(x). $$$$

Lean4

/-- `ArchimedeanClass.mk` defines an `AddValuation` on the ring `R`. -/
noncomputable def addValuation : AddValuation R (ArchimedeanClass R) :=
  AddValuation.of mk rfl rfl min_le_mk_add mk_mul

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