prodAssoc — Mathlib

English

The product of two modules is associative up to a natural linear isomorphism: ((M1 × M2) × M3) ≃ (M1 × (M2 × M3)).

Русский

Произведение модулей по существу ассоциативно: ((M1 × M2) × M3) эквивалентно (M1 × (M2 × M3)).

LaTeX

$$$((M_1 \times M_2) \times M_3) \cong_R (M_1 \times (M_2 \times M_3))$$$

Lean4

/-- Product of modules is associative up to linear isomorphism. -/
@[simps apply]
def prodAssoc (R M₁ M₂ M₃ : Type*) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁]
    [Module R M₂] [Module R M₃] : ((M₁ × M₂) × M₃) ≃ₗ[R] (M₁ × (M₂ × M₃)) :=
  { AddEquiv.prodAssoc with map_smul' := fun _r ⟨_m, _n⟩ => rfl }

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