mulRingNormEquivAbsoluteValue_apply

English

For any N: MulRingNorm R and x ∈ R, the equivalence sends x to the same value as N, i.e., mulRingNormEquivAbsoluteValue N x = N x.

Русский

Пусть N: MulRingNorm R и x ∈ R. Преобразование эквивальентности возвращает такое же значение, что и N: mulRingNormEquivAbsoluteValue N x = N x.

LaTeX

$$$ mulRingNormEquivAbsoluteValue\, N\, x = N\, x $$$

Lean4

theorem mulRingNormEquivAbsoluteValue_apply (N : MulRingNorm R) (x : R) : mulRingNormEquivAbsoluteValue N x = N x :=
  rfl

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