uniqueAddEquiv — Mathlib

English

There exists a canonical additive equivalence between the matrix bimodule M_{m,n}(A) and A when m and n are unique, preserving addition.

Русский

Существует каноническое аддитивное эквивалентное отображение между матричной многозначностью M_{m,n}(A) и A при уникальности индексов, сохраняющее сложение.

LaTeX

$$$\text{uniqueAddEquiv}:\; Matrix m n A \simeq_{+} A$ for unique m,n$$

Lean4

/-- The obvious additive isomorphism between M₁(A) and A, if A has an addition. -/
@[simps!]
def uniqueAddEquiv [Add A] : Matrix m n A ≃+ A where
  __ := uniqueEquiv
  map_add' := by simp

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