uniqueAlgEquiv — Mathlib

English

There is a canonical algebra isomorphism between Matrix m m A and A, given A is an algebra over R and m is unique, compatible with the existing ring and additive structure.

Русский

Существует каноническое алгебраическое изоморфизм между Matrix m m A и A при условии, что A — алгебра над R и m уникален, совместимый с существующей структурой кольца и сложения.

LaTeX

$$$\text{uniqueAlgEquiv}:\; Matrix m m A \cong_{R} A$$$

Lean4

/-- `M₁(A)` is equivalent to `A` as an `R`-algebra. -/
@[simps!]
def uniqueAlgEquiv [Semiring A] [CommSemiring R] [Algebra R A] : Matrix m m A ≃ₐ[R] A
    where
  __ := uniqueRingEquiv
  commutes' r := by aesop

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