instIsScalarTower — Mathlib

English

There is a SMulMemClass S M α if S ⊆ α, SMul M N, and IsScalarTower M N α with SMulMemClass S N α; smul_mem is given by smul_one_smul.

Русский

Существует SMulMemClass S M α при заданных условиях; smul_mem определяется через smul_one_smul.

LaTeX

$$$\\text{SMulMemClass } S M α$$$

Lean4

instance instIsScalarTower [Mul M] [MulMemClass S M] [IsScalarTower R M M] (s : S) : IsScalarTower R s s where
  smul_assoc r x y := Subtype.ext <| smul_assoc r (x : M) (y : M)

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