Commit 2023-07-15 00:02 6b711d2b

feat(data/matrix/auto): lemmas for arbitrary concrete matrices generated via auto_params (#15738) This adds a lemma matrix.mul_fin that works for arbitrary dimensions of concrete matrices indexed by fin. It uses a similar strategy to category_theory.reassoc_of to have a tactic populate wildcards in the lemma statement. For example:

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 mul_fin,
end
example {α} [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
  !![a₁₁, a₁₂] ⬝ !![b₁₁, b₁₂;
                    b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂;] :=
begin
  rw mul_fin,
end

Relevant zulip threads:

• Explicit vector unfolding
• concrete matrix multiplication
• A tactic for expanding matrices into coefficients