mathlib3 documentation

Automatically generated lemmas for working with concrete matrices #

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

This file contains "magic" lemmas which autogenerate to the correct size of matrix. For instance, matrix.of_mul_of_fin can be used as:

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₂₂] :=
  rw of_mul_of_fin,

Main results #

def fin.mmap {α : Type u_1} {n : } {m : Type u_1 Type u_2} [monad m] (f : fin n m α) :
m (fin n α)

Like list.mmap but for a vector.

meta def matrix.fin_eta.prove (m n : ) :

Prove a statement of the form ∀ A : matrix m n α, A = !![A 0 0, ...]. Returns the type of this statement and its proof.

Helper tactic used as an auto_param for matrix.fin_eta

theorem matrix.fin_eta {α : Type u_1} {m n : } (A : matrix (fin m) (fin n) α) {!![A 0 0, ...] : matrix (fin m) (fin n) α} (h : A = «!![A 0 0, ...]» . "derive") :
A = «!![A 0 0, ...]»

This lemma expands A into !![A 0 0, ...].

meta def matrix.fin_to_pexpr {m n : } (A : matrix (fin m) (fin n) pexpr) :

pi_fin.to_pexpr but for matrices

theorem matrix.of_mul_of_fin_aux (l m n : ) ⦃α : Type u_1⦄ [has_mul α] [add_comm_monoid α] :
matrix.forall (λ (A : matrix (fin l) (fin m) α), matrix.forall (λ (B : matrix (fin m) (fin n) α), A.mul B = A.mulᵣ B))

This statement is defeq to of_mul_of_fin, but syntactically worse

meta def matrix.of_mul_of_fin.prove (l m n : ) :

Prove a statement of the form

 α [has_mul α] [add_comm_monoid α] (a₁₁ ... aₗₘ b₁₁ ... bₘₙ : α),
   !![a₁₁  aₗₘ]  !![b₁₁  bₘₙ] = !![]

Returns the type of this statement and its proof.

Helper tactic used as an auto_param for matrix.of_mul_of_fin

theorem matrix.of_mul_of_fin {α : Type u_1} [has_mul α] [add_comm_monoid α] {l m n : } {a_coeffs : fin l fin m α} {b_coeffs : fin m fin n α} {ab_coeffs : fin l fin n α} (h : (matrix.of a_coeffs).mul (matrix.of b_coeffs) = matrix.of ab_coeffs . "derive") :
(matrix.of a_coeffs).mul (matrix.of b_coeffs) = matrix.of ab_coeffs

This lemma assumes that a_coeffs and b_coeffs refer to expressions of the form ![![x₀₀, x₀₁], ![x₁₀, x₁₁]]. It then uses an auto_param to populate ab_coeffs with an expression of the same form, containing the appropriate expressions in terms of +, *, aᵢⱼ, and bⱼₖ.