mulLeftMap_apply_single — Mathlib

English

If all pairs of left and right factors commute, then mulLeftMap equals mulRightMap.

Русский

Если все пары элементов слева и справа коммутируют, то mulLeftMap совпадает с mulRightMap.

LaTeX

$$$\forall\\{R\\} {S} [CommSemiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] (M : Submodule R S) (N : Submodule R S) (ι : Type*) (m : ι \to M), mulLeftMap N m = mulRightMap N m$$$

Lean4

@[simp]
theorem mulLeftMap_apply_single {M N : Submodule R S} {ι : Type*} (m : ι → M) (i : ι) (n : N) :
    mulLeftMap N m (Finsupp.single i n) = (m i).1 * n.1 := by simp [mulLeftMap]

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