Theorems · Definition · linear algebra

Matrix.uniqueAddEquiv

{m : Type u_1} → {n : Type u_2} → {A : Type u_3} → [Unique m] → [Unique n] → [inst : Add A] → Matrix m n A ≃+ A

The obvious additive isomorphism between M₁(A) and A, if A has an addition.

Defined in

Mathlib.LinearAlgebra.Matrix.Unique

Cited by

4 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

UniqueUniqueAdd