Documentation

Mathlib.Data.Matrix.Reflection

Lemmas for concrete matrices Matrix (Fin m) (Fin n) α #

This file contains alternative definitions of common operators on matrices that expand definitionally to the expected expression when evaluated on !![] notation.

This allows "proof by reflection", where we prove A = !![A 0 0, A 0 1; A 1 0, A 1 1] by defining Matrix.etaExpand A to be equal to the RHS definitionally, and then prove that A = eta_expand A.

The definitions in this file should normally not be used directly; the intent is for the corresponding *_eq lemmas to be used in a place where they are definitionally unfolded.

Main definitions #

def Matrix.Forall {α : Type u_1} {m : } {n : } :
(Matrix (Fin m) (Fin n) αProp)Prop

with better defeq for ∀ x : Matrix (Fin m) (Fin n) α, P x.

Equations
Instances For
    theorem Matrix.forall_iff {α : Type u_1} {m : } {n : } (P : Matrix (Fin m) (Fin n) αProp) :
    Matrix.Forall P ∀ (x : Matrix (Fin m) (Fin n) α), P x

    This can be use to prove

    example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
      (∀ x, P x) ↔ ∀ a b c d e f, P !![a, b, c; d, e, f] :=
    (forall_iff _).symm
    
    def Matrix.Exists {α : Type u_1} {m : } {n : } :
    (Matrix (Fin m) (Fin n) αProp)Prop

    with better defeq for ∃ x : Matrix (Fin m) (Fin n) α, P x.

    Equations
    Instances For
      theorem Matrix.exists_iff {α : Type u_1} {m : } {n : } (P : Matrix (Fin m) (Fin n) αProp) :
      Matrix.Exists P ∃ (x : Matrix (Fin m) (Fin n) α), P x

      This can be use to prove

      example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
        (∃ x, P x) ↔ ∃ a b c d e f, P !![a, b, c; d, e, f] :=
      (exists_iff _).symm
      
      def Matrix.transposeᵣ {α : Type u_1} {m : } {n : } :
      Matrix (Fin m) (Fin n) αMatrix (Fin n) (Fin m) α

      Matrix.transpose with better defeq for Fin

      Equations
      Instances For
        @[simp]
        theorem Matrix.transposeᵣ_eq {α : Type u_1} {m : } {n : } (A : Matrix (Fin m) (Fin n) α) :

        This can be used to prove

        example (a b c d : α) : transpose !![a, b; c, d] = !![a, c; b, d] := (transposeᵣ_eq _).symm
        
        def Matrix.dotProductᵣ {α : Type u_1} [Mul α] [Add α] [Zero α] {m : } (a : Fin mα) (b : Fin mα) :
        α

        Matrix.dotProduct with better defeq for Fin

        Equations
        Instances For
          @[simp]
          theorem Matrix.dotProductᵣ_eq {α : Type u_1} [Mul α] [AddCommMonoid α] {m : } (a : Fin mα) (b : Fin mα) :

          This can be used to prove

          example (a b c d : α) [Mul α] [AddCommMonoid α] :
            dot_product ![a, b] ![c, d] = a * c + b * d :=
          (dot_productᵣ_eq _ _).symm
          
          def Matrix.mulᵣ {l : } {m : } {n : } {α : Type u_1} [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) :
          Matrix (Fin l) (Fin n) α

          Matrix.mul with better defeq for Fin

          Equations
          Instances For
            @[simp]
            theorem Matrix.mulᵣ_eq {l : } {m : } {n : } {α : Type u_1} [Mul α] [AddCommMonoid α] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) :
            Matrix.mulᵣ A B = A * B

            This can be used to prove

            example [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
              !![a₁₁, a₁₂;
                 a₂₁, a₂₂] * !![b₁₁, b₁₂;
                                b₂₁, b₂₂] =
              !![a₁₁*b₁₁ + a₁₂*b₂₁, a₁₁*b₁₂ + a₁₂*b₂₂;
                 a₂₁*b₁₁ + a₂₂*b₂₁, a₂₁*b₁₂ + a₂₂*b₂₂] :=
            (mulᵣ_eq _ _).symm
            
            def Matrix.mulVecᵣ {l : } {m : } {α : Type u_1} [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (v : Fin mα) :
            Fin lα

            Matrix.mulVec with better defeq for Fin

            Equations
            Instances For
              @[simp]
              theorem Matrix.mulVecᵣ_eq {l : } {m : } {α : Type u_1} [NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin mα) :

              This can be used to prove

              example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
                !![a₁₁, a₁₂;
                   a₂₁, a₂₂] *ᵥ ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
              (mulVecᵣ_eq _ _).symm
              
              def Matrix.vecMulᵣ {l : } {m : } {α : Type u_1} [Mul α] [Add α] [Zero α] (v : Fin lα) (A : Matrix (Fin l) (Fin m) α) :
              Fin mα

              Matrix.vecMul with better defeq for Fin

              Equations
              Instances For
                @[simp]
                theorem Matrix.vecMulᵣ_eq {l : } {m : } {α : Type u_1} [NonUnitalNonAssocSemiring α] (v : Fin lα) (A : Matrix (Fin l) (Fin m) α) :

                This can be used to prove

                example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
                  ![b₁, b₂] ᵥ* !![a₁₁, a₁₂;
                                       a₂₁, a₂₂] = ![b₁*a₁₁ + b₂*a₂₁, b₁*a₁₂ + b₂*a₂₂] :=
                (vecMulᵣ_eq _ _).symm
                
                def Matrix.etaExpand {α : Type u_1} {m : } {n : } (A : Matrix (Fin m) (Fin n) α) :
                Matrix (Fin m) (Fin n) α

                Expand A to !![A 0 0, ...; ..., A m n]

                Equations
                Instances For
                  theorem Matrix.etaExpand_eq {α : Type u_1} {m : } {n : } (A : Matrix (Fin m) (Fin n) α) :

                  This can be used to prove

                  example (A : Matrix (Fin 2) (Fin 2) α) :
                    A = !![A 0 0, A 0 1;
                           A 1 0, A 1 1] :=
                  (etaExpand_eq _).symm