uniqueRingEquiv — Mathlib

English

There is a ring (or nonunital semiring) isomorphism between Matrix m m A and A, respecting the ring operations, provided m is unique.

Русский

Существует изоморфизм колец между Matrix m m A и A, сохраняющий операции сложения и умножения, если m уникален.

LaTeX

$$$\text{uniqueRingEquiv}:\; Matrix m m A \cong^{+}_{?} A$$$

Lean4

/-- `M₁(A)` and `A` are equivalent as rings. -/
@[simps!]
def uniqueRingEquiv [NonUnitalNonAssocSemiring A] : Matrix m m A ≃+* A
    where
  __ := uniqueAddEquiv
  map_mul' := by simp [mul_apply]

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