val_neg — Mathlib

English

Negating a unit and then taking its underlying value corresponds to taking the additive inverse of the underlying element.

Русский

Отрицание единицы и последующее извлечение основания даёт аддитивную инверсию элемента.

LaTeX

$$$\uparrow(-u) = -\uparrow u$$$

Lean4

/-- Representing an element of a ring's unit group as an element of the ring commutes with
mapping this element to its additive inverse. -/
@[simp, norm_cast]
protected theorem val_neg (u : αˣ) : (↑(-u) : α) = -u :=
  rfl

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