mulLeftMap_eq_mulRightMap — Mathlib

English

If each pair (m_i, n) commutes, then mulLeftMap equals mulRightMap.

Русский

Если каждая пара (m_i, n) коммутирует, то mulLeftMap равен mulRightMap.

LaTeX

$$mulLeftMap_eq_mulRightMap_of_commute {R : Type*} [Semiring R] {S : Type*} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower 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$$

Lean4

theorem mulLeftMap_eq_mulRightMap {S : Type*} [CommSemiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S]
    [IsScalarTower R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M) :
    mulLeftMap N m = mulRightMap N m :=
  mulLeftMap_eq_mulRightMap_of_commute N m fun _ _ ↦ mul_comm _ _

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