mulRingNormEquivAbsoluteValue_symm_apply

English

Let R be a ring and v an absolute value on R. Then applying the inverse of the natural equivalence between MulRingNorms and AbsoluteValues yields the same value on any x; i.e. mulRingNormEquivAbsoluteValue.symm v x = v x.

Русский

Пусть R — кольцо и v — абсолютная величина на R. Тогда применение обратного отображения эквивалентности между MulRingNorm и AbsoluteValue к v на элементе x даёт такое же значение: mulRingNormEquivAbsoluteValue.symm v x = v x.

LaTeX

$$$mulRingNormEquivAbsoluteValue.symm\, v\, x = v\, x$$$

Lean4

theorem mulRingNormEquivAbsoluteValue_symm_apply (v : AbsoluteValue R ℝ) (x : R) :
    mulRingNormEquivAbsoluteValue.symm v x = v x :=
  rfl

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