setSemiring_smul_def — Mathlib

English

The action of a SetSemiring on Submodule is given by the product with the span of the down-set; i.e. s • P = span R (down s) * P.

Русский

Действие множества SetSemiring на подмодуль задаётся как произведение образованного замыкания: s • P = span R (down s) * P.

LaTeX

$$$s \cdot P = \mathrm{span}\,R(\mathrm{SetSemiring.down}\,s) \cdot P$$$

Lean4

theorem setSemiring_smul_def (s : SetSemiring A) (P : Submodule R A) :
    s • P = span R (SetSemiring.down (α := A) s) * P :=
  rfl

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