trivial — Mathlib

English

The trivial absolute value maps every nonzero element to 1; 0 maps to 0.

Русский

Тривиальное абсолютное значение отправляет каждое ненулевое элемент на 1, 0 на 0.

LaTeX

$$$\\operatorname{AbsoluteValue.trivial}(x) = \\begin{cases}0, & x=0 \\\\ 1, & x\\neq 0\\end{cases}$$$

Lean4

/-- The *trivial* absolute value takes the value `1` on all nonzero elements. -/
protected def trivial : AbsoluteValue R S
    where
  toFun x := if x = 0 then 0 else 1
  map_mul' x
    y := by
    rcases eq_or_ne x 0 with rfl | hx
    · simp
    rcases eq_or_ne y 0 with rfl | hy
    · simp
    simp [hx, hy]
  nonneg' x := by rcases eq_or_ne x 0 with hx | hx <;> simp [hx]
  eq_zero' x := by rcases eq_or_ne x 0 with hx | hx <;> simp [hx]
  add_le' x
    y := by
    rcases eq_or_ne x 0 with rfl | hx
    · simp
    rcases eq_or_ne y 0 with rfl | hy
    · simp
    simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]
    rcases eq_or_ne (x + y) 0 with hxy | hxy <;> simp [hxy, one_le_two]

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