map_neg — Mathlib

English

For any abv : AbsoluteValue R S, and any a ∈ R, abv(−a) = abv(a).

Русский

Для любого модульного отображения abv: AbsoluteValue R S и любого a ∈ R выполняется abv(−a) = abv(a).

LaTeX

$$$\\forall a \\in R, \\operatorname{abv}(-a) = \\operatorname{abv}(a)$$$

Lean4

@[simp]
protected theorem map_neg (a : R) : abv (-a) = abv a :=
  by
  by_cases ha : a = 0; · simp [ha]
  refine (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_
  exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'

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