compatibleSMul — Mathlib

English

Given SMul R S and IsScalarTower relations, there is a CompatibleSMul structure on M and M₂ over R and S, ensuring the action is compatible via fₗ.

Русский

При наличии SMul R S и отношений IsScalarTower между R, S и модулями M, M₂, существует структура CompatibleSMul на M и M₂ над R и S, обеспечивающая совместимость действия через fₗ.

LaTeX

$$$ \text{CompatibleSMul } M M_2 R S $ with$$

Lean4

instance (priority := 100) compatibleSMul [SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂] :
    CompatibleSMul M M₂ R S :=
  ⟨fun fₗ c x ↦ by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]⟩

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