prodComm — Mathlib

English

The product of two modules is commutative up to continuous linear isomorphism: M1 × M2 ≃L[R] M2 × M1.

Русский

Произведение модулей допускает коммутативность до непрерывного линейного эквивалента: M1 × M2 ≃L[R] M2 × M1.

LaTeX

$$$$ (M_1 \times M_2) \simeq_L[R] (M_2 \times M_1). $$$$

Lean4

/-- Product of modules is commutative up to continuous linear isomorphism. -/
@[simps! apply toLinearEquiv]
def prodComm [Module R₁ M₂] : (M₁ × M₂) ≃L[R₁] M₂ × M₁ :=
  { LinearEquiv.prodComm R₁ M₁ M₂ with
    continuous_toFun := continuous_swap
    continuous_invFun := continuous_swap }

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