prodComm — Mathlib

English

Product of modules is commutative up to linear isomorphism; M × N is linearly isomorphic to N × M via swapping components.

Русский

Произведение модулей коммутирует до линейного изоморфизма: M × N изоморфно по линейному отображению N × M (меняя местами компоненты).

LaTeX

$$$ (M \times N) \cong_R (N \times M)$$$

Lean4

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

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