English
Let m and n be finite index types, and let A, B be algebras over R with S, etc., as in the setup of the Kronecker-mul equivalence. Then the inverse (symm) of the algebraic Kronecker mul equivalence coincides with the inverse (symm) of the corresponding linear Kronecker mul equivalence on every matrix x; i.e. the two inverse identifications agree on all x.
Русский
Пусть m, n — конечные индексовые типы, A и B — алгебры над R и заданы условия существования эквивалентов Кронекера. Тогда обратный отображатель алгебраического изоморфизма Kronecker-множителя совпадает с обратным линейного Kronecker-изоморфизма на каждом элементе x; т.е. две соответствующие обратные идентификации совпадают на любом x.
LaTeX
$$$((kroneckerTMulAlgEquiv\; m\; n\; R\; S\; A\; B).\\mathrm{symm})\\,x = ((kroneckerTMulLinearEquiv\; m\; m\; n\; n\; R\; S\; A\; B).\\mathrm{symm})\\,x$$$
Lean4
@[simp]
theorem kroneckerTMulAlgEquiv_symm_apply (x : Matrix (m × n) (m × n) (A ⊗[R] B)) :
(kroneckerTMulAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x :=
rfl
