instAlgebraOfNatENNRealUnitizationOfIsScalarTower

English

For any suitable commutative semiring R with a 𝕜-algebra structure and compatible actions on A, WithLp 1 (Unitization 𝕜 A) carries an Algebra R structure.

Русский

Пусть для любого подходящего условного полупрямоугольника R есть структура алгебры над R, совместимая с 𝕜, тогда WithLp 1 (Unitization 𝕜 A) имеет алгебру над R.

LaTeX

$$$\text{WithLp } 1 (Unitization 𝕜 A)\text{ is an } \mathsf{Algebra}_R(\text{WithLp } 1 (Unitization 𝕜 A))$$$

Lean4

instance {R : Type*} [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] :
    Algebra R (WithLp 1 (Unitization 𝕜 A)) :=
  inferInstanceAs (Algebra R (Unitization 𝕜 A))

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