instSMul — Mathlib

English

There is a canonical scalar multiplication of R on FreeAlgebra A X defined via the algebra map and quotient construction.

Русский

Существует каноническое действие скаляров R на FreeAlgebra A X через алгебраическое отображение и факторизацию по отношению эквивалентности.

LaTeX

$$instance instSMul {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where smul r := Quot.map (HMul.hMul (algebraMap R A r : Pre A X)) fun _ _ ↦ Rel.mul_compat_right$$

Lean4

instance instSMul {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
  smul r := Quot.map (HMul.hMul (algebraMap R A r : Pre A X)) fun _ _ ↦ Rel.mul_compat_right

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