# mathlib3documentation

data.matrix.reflection

# Lemmas for concrete matrices matrix (fin m) (fin n) α#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.eta_expand 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 definitionss #

• matrix.transposeᵣ
• matrix.dot_productᵣ
• matrix.mulᵣ
• matrix.mul_vecᵣ
• matrix.vec_mulᵣ
• matrix.eta_expand
def matrix.forall {α : Type u_1} {m n : } (P : matrix (fin m) (fin n) α Prop) :
Prop

∀ with better defeq for ∀ x : matrix (fin m) (fin n) α, P x.

Equations
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 : } (P : matrix (fin m) (fin n) α Prop) :
Prop

∃ with better defeq for ∃ x : matrix (fin m) (fin n) α, P x.

Equations
theorem matrix.exists_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] :=
(exists_iff _).symm

def matrix.transposeᵣ {α : Type u_1} {m n : } :
matrix (fin m) (fin n) α matrix (fin n) (fin m) α

matrix.tranpose with better defeq for fin

Equations
@[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.dot_productᵣ {α : Type u_1} [has_mul α] [has_add α] [has_zero α] {m : } (a b : fin m α) :
α

matrix.dot_product with better defeq for fin

Equations
@[simp]
theorem matrix.dot_productᵣ_eq {α : Type u_1} [has_mul α] {m : } (a b : fin m α) :

This can be used to prove

example (a b c d : α) [has_mul α] [add_comm_monoid α] :
dot_product ![a, b] ![c, d] = a * c + b * d :=
(dot_productᵣ_eq _ _).symm

def matrix.mulᵣ {l m n : } {α : Type u_1} [has_mul α] [has_add α] [has_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
@[simp]
theorem matrix.mulᵣ_eq {l m n : } {α : Type u_1} [has_mul α] (A : matrix (fin l) (fin m) α) (B : matrix (fin m) (fin n) α) :
A.mulᵣ B = A.mul B

This can be used to prove

example [add_comm_monoid α] [has_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.mul_vecᵣ {l m : } {α : Type u_1} [has_mul α] [has_add α] [has_zero α] (A : matrix (fin l) (fin m) α) (v : fin m α) :
fin l α

matrix.mul_vec with better defeq for fin

Equations
@[simp]
theorem matrix.mul_vecᵣ_eq {l m : } {α : Type u_1} (A : matrix (fin l) (fin m) α) (v : fin m α) :

This can be used to prove

example [non_unital_non_assoc_semiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
!![a₁₁, a₁₂;
a₂₁, a₂₂].mul_vec ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
(mul_vecᵣ_eq _ _).symm

def matrix.vec_mulᵣ {l m : } {α : Type u_1} [has_mul α] [has_add α] [has_zero α] (v : fin l α) (A : matrix (fin l) (fin m) α) :
fin m α

matrix.vec_mul with better defeq for fin

Equations
@[simp]
theorem matrix.vec_mulᵣ_eq {l m : } {α : Type u_1} (v : fin l α) (A : matrix (fin l) (fin m) α) :
=

This can be used to prove

example [non_unital_non_assoc_semiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
vec_mul ![b₁, b₂] !![a₁₁, a₁₂;
a₂₁, a₂₂] = ![b₁*a₁₁ + b₂*a₂₁, b₁*a₁₂ + b₂*a₂₂] :=
(vec_mulᵣ_eq _ _).symm

def matrix.eta_expand {α : 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
theorem matrix.eta_expand_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] :=
(eta_expand_eq _).symm