Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-15 00:02 6b711d2b

View on Github →

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

Relevant zulip threads:

Estimated changes