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

source
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
    Instances For
      source
      @[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
      source
      @[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) :
      uniqueEquiv M = M default default
      source
      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
        Instances For
          source
          @[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) :
          uniqueAddEquiv M = M default default
          source
          @[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
          source
          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
            Instances For
              source
              @[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) :
              uniqueLinearEquiv.symm a✝ = uniqueAddEquiv.invFun a✝
              source
              @[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) :
              uniqueLinearEquiv a✝ = uniqueAddEquiv.toFun a✝
              source
              def Matrix.uniqueRingEquiv {m : Type u_1} {A : Type u_3} [Unique m] [NonUnitalNonAssocSemiring A] :
              Matrix m m A ≃+* A

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

              Equations
                Instances For
                  source
                  @[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
                  source
                  @[simp]
                  theorem Matrix.uniqueRingEquiv_apply {m : Type u_1} {A : Type u_3} [Unique m] [NonUnitalNonAssocSemiring A] (M : Matrix m m A) :
                  uniqueRingEquiv M = M default default
                  source
                  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
                    Instances For
                      source
                      @[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
                      source
                      @[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) :
                      uniqueAlgEquiv M = M default default