English
For any e: n ≃ p and t: TransvectionStruct n R, the matrix toMatrix of the reindexed transvection equals the corresponding AlgEquiv image of t.toMatrix under the reindexing equivalence.
Русский
Для любого e: n ≃ p и t: TransvectionStruct n R матрица toMatrix преобразованной трансвеκции равна образу по эквивалентности перепозиционирования.
LaTeX
$$$(t.reindexEquiv e).toMatrix = \\operatorname{reindexAlgEquiv}(R,R,e)(t.toMatrix)$$$
Lean4
theorem toMatrix_reindexEquiv (e : n ≃ p) (t : TransvectionStruct n R) :
(t.reindexEquiv e).toMatrix = reindexAlgEquiv R _ e t.toMatrix :=
by
rcases t with ⟨t_i, t_j, _⟩
ext a b
simp only [reindexEquiv, transvection, toMatrix_mk, submatrix_apply, reindex_apply, reindexAlgEquiv_apply]
by_cases ha : e t_i = a <;> by_cases hb : e t_j = b <;> by_cases hab : a = b <;>
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]
