apply_one — Mathlib

English

For the unit element 1 in the structure of a nonarchimedean additive norm, its evaluation at x is 0 if x = 0 and 1 otherwise; i.e., the unit acts as the indicator of nonzero elements.

Русский

Для единичного элемента 1 в структуре немонтоничного аддитивного нормирования значение на x равно 0, если x = 0, и 1 в противном случае; т. е. единичка действует как индикатор ненулевых элементов.

LaTeX

$$$ (1 : \\text{NonarchAddGroupNorm } E) x = \\begin{cases}0, & x = 0 \\\\\\ 1, & x \\neq 0. \\end{cases} $$$

Lean4

@[simp]
theorem apply_one [DecidableEq E] (x : E) : (1 : NonarchAddGroupNorm E) x = if x = 0 then 0 else 1 :=
  rfl

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