instAlgebra_right — Mathlib

English

WithAbs v carries an algebra structure over R; i.e., it is an R-algebra when v is an absolute value on R′ into S.

Русский

WithAbs v наделено алгебрной структурой над R; то есть WithAbs v является R-алгеброй, когда v — абсолютная величина на R′ в S.

LaTeX

$$$Algebra\\,R\\,(WithAbs\\,v)$$$

Lean4

instance instAlgebra_right (v : AbsoluteValue R' S) : Algebra R (WithAbs v) :=
  inferInstanceAs <| Algebra R R'

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