equiv_algebraMap_apply — Mathlib

English

The equiv relates two algebra maps across changes of base: equiv w (algebraMap (WithAbs v) (WithAbs w) x) equals algebraMap R R' (equiv v x).

Русский

Эквивалентность связывает два отображения алгебры через базисные изменения: equiv w (algebraMap (WithAbs v) (WithAbs w) x) = algebraMap R R' (equiv v x).

LaTeX

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

Lean4

theorem equiv_algebraMap_apply (v : AbsoluteValue R S) (w : AbsoluteValue R' S) (x : WithAbs v) :
    equiv w (algebraMap (WithAbs v) (WithAbs w) x) = algebraMap R R' (equiv v x) :=
  rfl

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