Documentation

Mathlib.LinearAlgebra.Matrix.Unique

One by one matrices #

This file proves that one by one matrices over a base are equivalent to the base itself under the canonical map that sends a one by one matrix !![a] to a.

Main results #

Tags #

Matrix, Unique, AlgEquiv

def Matrix.uniqueEquiv {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] :
Matrix m n A A

The isomorphism between the type of all one by one matrices and the base type.

Equations
@[simp]
theorem Matrix.uniqueEquiv_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] (a : A) :
uniqueEquiv.symm a = of fun (x : m) (x : n) => a
@[simp]
theorem Matrix.uniqueEquiv_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] (M : Matrix m n A) :
def Matrix.uniqueAddEquiv {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] [Add A] :
Matrix m n A ≃+ A

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

Equations
@[simp]
theorem Matrix.uniqueAddEquiv_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] [Add A] (M : Matrix m n A) :
@[simp]
theorem Matrix.uniqueAddEquiv_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique m] [Unique n] [Add A] (a : A) :
uniqueAddEquiv.symm a = of fun (x : m) (x : n) => a
def Matrix.uniqueLinearEquiv {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [Unique m] [Unique n] [Semiring R] [AddCommMonoid A] [Module R A] :
Matrix m n A ≃ₗ[R] A

M₁(A) is linearly equivalent to A as an R-module where R is a semiring.

Equations
@[simp]
theorem Matrix.uniqueLinearEquiv_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [Unique m] [Unique n] [Semiring R] [AddCommMonoid A] [Module R A] (a✝ : A) :
@[simp]
theorem Matrix.uniqueLinearEquiv_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_4} [Unique m] [Unique n] [Semiring R] [AddCommMonoid A] [Module R A] (a✝ : Matrix m n A) :

M₁(A) and A are equivalent as rings.

Equations
@[simp]
theorem Matrix.uniqueRingEquiv_symm_apply {m : Type u_1} {A : Type u_3} [Unique m] [NonUnitalNonAssocSemiring A] (a : A) :
uniqueRingEquiv.symm a = of fun (x x : m) => a
def Matrix.uniqueAlgEquiv {m : Type u_1} {A : Type u_3} {R : Type u_4} [Unique m] [Semiring A] [CommSemiring R] [Algebra R A] :
Matrix m m A ≃ₐ[R] A

M₁(A) is equivalent to A as an R-algebra.

Equations
@[simp]
theorem Matrix.uniqueAlgEquiv_symm_apply {m : Type u_1} {A : Type u_3} {R : Type u_4} [Unique m] [Semiring A] [CommSemiring R] [Algebra R A] (a : A) :
uniqueAlgEquiv.symm a = of fun (x x : m) => a
@[simp]
theorem Matrix.uniqueAlgEquiv_apply {m : Type u_1} {A : Type u_3} {R : Type u_4} [Unique m] [Semiring A] [CommSemiring R] [Algebra R A] (M : Matrix m m A) :