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
🔸 coverage
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.

Instances For
    source
    📐 coverage
    @[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
    📐 coverage
    @[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_1 : n) => a
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[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
      📐 coverage
      @[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_1 : n) => a
      source
      🔸 coverage
      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.

      Instances For
        source
        📐 coverage
        @[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
        📐 coverage
        @[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
        🔸 coverage
        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.

        Instances For
          source
          📐 coverage
          @[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
          📐 coverage
          @[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_1 : m) => a
          source
          🔸 coverage
          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.

          Instances For
            source
            📐 coverage
            @[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
            source
            📐 coverage
            @[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_1 : m) => a