Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] left vector multiplication not associative (a ...

Email Gateway (Sep 17 2024 at 07:22):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,

in HOL/Analysis/Finite_Cartesian_Product.thy
the multiplication by a vector from the left  (constant
vector_matrix_mult) is not associative unless the underlying semiring is
commutative.
Namely,
  lemma  "(x v* A) v* B = x v* (A ** B)"
is not true, unlike its proven counterpart
lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"

This is due to the inverted order of multiplicands in the definition of
vector_matrix_mult.

I expect this is unintended. If there is no motivation I miss, I suggest
it should be changed.

Best regards

Stepan

Last updated: Jan 04 2025 at 20:18 UTC