instIsScalarTower — Mathlib

English

If α acts on A and on Submodules of A compatibly, then α acts on Submodule R A via pointwise actions, forming a scalar tower: smul_assoc a S T holds.

Русский

Если α действует на A и на подмодули A совместимо, то α действует на Submodule R A по точечному действию, образуя скалярную башню: smul_assoc a S T.

LaTeX

$$$\\text{smul\_assoc}\\; a\\; S\\; T$$

Lean4

instance [IsScalarTower α A A] : IsScalarTower α (Submodule R A) (Submodule R A) where
  smul_assoc a S
    T := by
    rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span, smul_span,
      smul_mul_assoc]

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