English
The updateRow of the identity equals the transvection: updateRow(I,i, I_i + c I_j) = T_{ij}(c).
Русский
Обновление строки для I даёт транспекцию: updateRow(I,i, I_i + c I_j) = T_{ij}(c).
LaTeX
$$$$ \\operatorname{updateRow}(I_n, i, I_n i + c \\cdot I_n j) = \\mathrm{transvection}_{ij}(c). $$$$
Lean4
/-- A transvection matrix is obtained from the identity by adding `c` times the `j`-th row to
the `i`-th row. -/
theorem updateRow_eq_transvection [Finite n] (c : R) :
updateRow (1 : Matrix n n R) i ((1 : Matrix n n R) i + c • (1 : Matrix n n R) j) = transvection i j c :=
by
cases nonempty_fintype n
ext a b
by_cases ha : i = a
· by_cases hb : j = b
·
simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte, smul_eq_mul, mul_one,
transvection, add_apply, single_apply_same]
·
simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte, smul_eq_mul, mul_zero,
add_zero, transvection, add_apply, and_false, not_false_eq_true, single_apply_of_ne]
·
simp only [updateRow_ne, transvection, ha, Ne.symm ha, single_apply_of_ne, add_zero, Ne, not_false_iff, false_and,
add_apply]
