Theorems · Theorem · order theory

AbsoluteValue.map_neg

∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  (abv : AbsoluteValue R S) [NoZeroDivisors S] (a : R), abv (-a) = abv a

Defined in

Mathlib.Algebra.Order.AbsoluteValue.Basic

Cited by

4 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingPartialOrderIsOrderedRingRingNoZeroDivisors