mathlib3 documentation

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 #

source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem matrix.transposeᵣ_eq {α : Type u_1} {m n : ℕ} (A : matrix (fin m) (fin n) α) :
A.transposeᵣ = A.transpose

This can be used to prove

example (a b c d : α) : transpose !![a, b; c, d] = !![a, c; b, d] := (transposeᵣ_eq _).symm
source
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
source
@[simp]
theorem matrix.dot_productᵣ_eq {α : Type u_1} [has_mul α] [add_comm_monoid α] {m : ℕ} (a b : fin m → α) :
matrix.dot_productᵣ a b = matrix.dot_product a b

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
source
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
source
@[simp]
theorem matrix.mulᵣ_eq {l m n : ℕ} {α : Type u_1} [has_mul α] [add_comm_monoid α] (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
source
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
source
@[simp]
theorem matrix.mul_vecᵣ_eq {l m : ℕ} {α : Type u_1} [non_unital_non_assoc_semiring α] (A : matrix (fin l) (fin m) α) (v : fin m → α) :
A.mul_vecᵣ v = A.mul_vec v

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
source
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
source
@[simp]
theorem matrix.vec_mulᵣ_eq {l m : ℕ} {α : Type u_1} [non_unital_non_assoc_semiring α] (v : fin l → α) (A : matrix (fin l) (fin m) α) :
matrix.vec_mulᵣ v A = matrix.vec_mul v A

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
source
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
source
theorem matrix.eta_expand_eq {α : Type u_1} {m n : ℕ} (A : matrix (fin m) (fin n) α) :
A.eta_expand = A

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