mathlib

6b711d2b - feat(data/matrix/auto): lemmas for arbitrary concrete matrices generated via auto_params (#15738)

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: ```lean 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](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Explicit.20vector.20unfolding) * [concrete matrix multiplication](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/concrete.20matrix.20multiplication/near/291208624) * [A tactic for expanding matrices into coefficients](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/A.20tactic.20for.20expanding.20matrices.20into.20coefficients)