algebraMap_right_apply — Mathlib

English

Algebra maps are compatible on either side: algebraMap R (WithAbs v) x equals WithAbs.equiv v (algebraMap R R' x).

Русский

Совместимость отображения алгебры по обе стороны: algebraMap R (WithAbs v) x = WithAbs.equiv v (algebraMap R R' x).

LaTeX

$$$algebraMap\\,R\\,(WithAbs\\,v)\\,x = WithAbs.equiv\\,v\\,(algebraMap\\,R\\,R'\\,x)$$$

Lean4

theorem algebraMap_right_apply (v : AbsoluteValue R' S) (x : R) :
    algebraMap R (WithAbs v) x = WithAbs.equiv v (algebraMap R R' x) :=
  rfl

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