lsmul_flip_apply — Mathlib

English

The flipped left-smul map applied to m ∈ M is the span-singleton map sending r ∈ R to r m in M; i.e., (lsmul R M).flip m = toSpanSingleton R M m, which corresponds to the map r ↦ r m.

Русский

Перевёрнутое слева умножение на m, рассматриваемое как линейное отображение, совпадает с отображением r ↦ r m.

LaTeX

$$$$ (\mathrm{lsmul}\;R\;M)^{\mathrm{flip}}(m) = \mathrm{toSpanSingleton}_{R}^{M}(m) \;=\; (r \mapsto r m). $$$$

Lean4

@[simp]
theorem lsmul_flip_apply (m : M) : (lsmul R M).flip m = toSpanSingleton R M m :=
  rfl

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