apply_one — Mathlib

English

For every element x in R, the unit RingSeminorm (the one corresponding to 1) takes the value 0 at 0 and 1 at any nonzero element: (1 : RingSeminorm R) x = 0 if x = 0, and = 1 otherwise.

Русский

Для каждого x ∈ R единичная семинормA RingSeminorm даёт 0 при x = 0 и 1 при x ≠ 0: (1 : RingSeminorm R) x = 0, если x = 0; иначе = 1.

LaTeX

$$$ (1 : \mathrm{RingSeminorm\} R)\, x = \begin{cases}0,& x=0\\ 1,& x\neq 0\end{cases} $$$

Lean4

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

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