Absolute values of elements of finite order #
An absolute value with values in a linearly ordered ring takes the value 1 at every element of
finite multiplicative order, for instance at every root of unity of a field: if x ^ n = 1 with
n ≠ 0, then abv x ^ n = 1 with abv x ≥ 0, so abv x = 1.
@[simp]
theorem
AbsoluteValue.map_eq_one_of_isOfFinOrder
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Nontrivial R]
[Ring S]
[LinearOrder S]
[IsStrictOrderedRing S]
(abv : AbsoluteValue R S)
{x : R}
(hx : IsOfFinOrder x)
:
An absolute value takes the value 1 at every element of finite order.