English
The matrix of the embedded transvection on n ⊕ p equals the block matrix with t.toMatrix in the top-left block and 1 in the bottom-right corner.
Русский
Матрица вложенной трансвеκции на n ⊕ p равна блочно-диагональной матрице: t.toMatrix наверху и 1 в правом нижнем углу.
LaTeX
$$$(\\text{sumInl }p\\,t).\\text{toMatrix} = \\operatorname{fromBlocks}(t.toMatrix, 0, 0, 1)$$$
Lean4
theorem toMatrix_sumInl (t : TransvectionStruct n R) : (t.sumInl p).toMatrix = fromBlocks t.toMatrix 0 0 1 :=
by
cases t
ext a b
rcases a with a | a <;> rcases b with b | b
· by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h, single]
· simp [TransvectionStruct.sumInl, transvection]
· simp [TransvectionStruct.sumInl, transvection]
· by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h]
