unit — Mathlib

English

There is a distinguished unit in Γ₀ arising from a rank-one valuation, defined by evaluating a chosen nonzero element of R.

Русский

Существует выделенная единица в Γ₀, полученная из ранга одной оценки через выбранный ненулевой элемент кольца.

LaTeX

$$$\text{unit}(v) := \text{the unit of } Γ_0 \\text{corresponding to } v\big(\text{nontrivial}(v).choose\big).$$$

Lean4

/-- A nontrivial unit of `Γ₀`, given that there exists a rank one `v : Valuation R Γ₀`. -/
def unit : Γ₀ˣ :=
  Units.mk0 (v (nontrivial v).choose) ((nontrivial v).choose_spec).1

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