map_smul_of_tower — Mathlib

English

Let S be a commutative semiring, R an S-algebra, M,N modules over R with IsScalarTower S R M,N. Then for a ∈ S and x ∈ M, Q(a·x) = (a·a) · Q(x).

Русский

Пусть S — коммутативная полугруппа, R — алгебра над S, M,N моды над R и выполняется условие IsScalarTower S R M,N. Тогда для a ∈ S, x ∈ M выполняется Q(a·x) = (a^2)·Q(x).

LaTeX

$$∀ a ∈ S, ∀ x ∈ M, Q(a • x) = (a * a) • Q x$$

Lean4

theorem map_smul_of_tower [CommSemiring S] [Algebra S R] [SMul S M] [IsScalarTower S R M] [Module S N]
    [IsScalarTower S R N] (a : S) (x : M) : Q (a • x) = (a * a) • Q x := by
  rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← RingHom.map_mul, algebraMap_smul]

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