mathlib3 documentation

data.matrix.auto

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

Main results #

source
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.

Equations
source
meta def matrix.fin_eta.prove (m n : ℕ) :
tactic (expr × expr)

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

source
meta def matrix.fin_eta.derive  :
tactic unit

Helper tactic used as an auto_param for matrix.fin_eta

source
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, ...].

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

pi_fin.to_pexpr but for matrices

source
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

source
meta def matrix.of_mul_of_fin.prove (l m n : ℕ) :
tactic (expr × expr)

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.

source
meta def matrix.of_mul_of_fin.derive  :
tactic unit

Helper tactic used as an auto_param for matrix.of_mul_of_fin

source
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ⱼₖ.