# 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 #

• Matrix.transposeᵣ
• Matrix.dotProductᵣ
• Matrix.mulᵣ
• Matrix.mulVecᵣ
• Matrix.vecMulᵣ
• Matrix.etaExpand
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) :
(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) :
x, 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

Instances For
@[simp]
theorem Matrix.dotProductᵣ_eq {α : Type u_1} [Mul α] [] {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

Instances For
@[simp]
theorem Matrix.mulᵣ_eq {l : } {m : } {n : } {α : Type u_1} [Mul α] [] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) :
= 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

Instances For
@[simp]
theorem Matrix.mulVecᵣ_eq {l : } {m : } {α : Type u_1} (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₂₂].mulVec ![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

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

This can be used to prove

example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
vecMul ![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]

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