instAlgebra_left — Mathlib

English

WithAbs v can be given an algebra structure over R′; in other words, WithAbs v carries a canonical left R′-algebra structure extending the given R′-action.

Русский

WithAbs v может быть наделено структурой алгебры над R′; то есть WithAbs v естественным образом образует левую алгебру над R′, совместимую с данной действиeй R′.

LaTeX

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

Lean4

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

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