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 #
∀
with better defeq for ∀ x : Matrix (Fin m) (Fin n) α, P x
.
Equations
- Matrix.Forall x = x (↑Matrix.of ![])
- Matrix.Forall x = FinVec.Forall fun r => Matrix.Forall fun A => x (↑Matrix.of (Matrix.vecCons r A))
Instances For
∃
with better defeq for ∃ x : Matrix (Fin m) (Fin n) α, P x
.
Equations
- Matrix.Exists x = x (↑Matrix.of ![])
- Matrix.Exists x = FinVec.Exists fun r => Matrix.Exists fun A => x (↑Matrix.of (Matrix.vecCons r A))
Instances For
Matrix.transpose
with better defeq for Fin
Equations
- Matrix.transposeᵣ x_4 = ↑Matrix.of ![]
- Matrix.transposeᵣ A = ↑Matrix.of (Matrix.vecCons (FinVec.map (fun v => v 0) A) (Matrix.transposeᵣ (Matrix.submatrix A id Fin.succ)))
Instances For
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
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
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
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