Kronecker left and right cancel

Stream: mathlib4

[Michael Lan]

Hi! New-ish to Lean. I'm not very good at navigating the mathlib documentation; is there already proofs that matrices under the Kronecker product have left- and right- cancel?

More importantly, how would I navigate the site to be sure of things like this in the future?

[Gareth Ma]

For me I git clone'ed the entire source code of Mathlib locally, then use grep or VSCode's "search in project" feature + guessing the theorem name to find theorems.

Here are the results. It seems the result doesn't exist, but it should be easy to prove. I assume you mean $A \otimes B = A \otimes C \implies B = C$ if any element of $A$ is invertible?

image.png

[Michael Lan]

Yeah, I'll take a shot at it

[Eric Wieser]

If you want a spoiler, here's a very short proof:

example {l m n p R : Type*} [Mul R] (A : Matrix l m R) (i j) (hA : IsLeftRegular (A i j)) :
    Function.Injective fun B : Matrix n p R => A ⊗ₖ B :=
  fun _B _C h => Matrix.ext fun i' j' => hA <| congr_fun₂ h (i, i') (j, j')