mulLeftMap_eq_mulRightMap_of_commute

English

Under appropriate commutativity assumptions, the left and right sum maps coincide.

Русский

При соответствующих предположениях о коммутативности левые и правые суммы совпадают.

LaTeX

$$mulLeftMap_eq_mulRightMap {S : Type*} [CommSemiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M) : mulLeftMap N m = mulRightMap N m$$

Lean4

theorem mulLeftMap_eq_mulRightMap_of_commute [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type*}
    (m : ι → M) (hc : ∀ (i : ι) (n : N), Commute (m i).1 n.1) : mulLeftMap N m = mulRightMap N m := by ext i n;
  simp [(hc i n).eq]

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