mul_adjp_add_detp — Mathlib

English

If A·B = I (the identity in M_n), then for any i, j, k with i ≠ j, the scalar product A_{ik} · B_{kj} is an AddUnit; i.e., its sum behaves like a unit contribution.

Русский

Если A·B = I, то для любых i≠j сумма A_{ik} B_{kj} имеет свойство IsAddUnit (единичный вклад).

LaTeX

$$$A B = I_n \\Rightarrow \\forall i\\neq j, \\; IsAddUnit\\bigl(A_{ik} B_{kj}\\bigr)$$$

Lean4

theorem mul_adjp_add_detp : A * adjp 1 A + detp (-1) A • 1 = A * adjp (-1) A + detp 1 A • 1 :=
  by
  ext i j
  rcases eq_or_ne i j with rfl | h <;> simp_rw [add_apply, smul_apply, smul_eq_mul]
  · simp_rw [mul_adjp_apply_eq, one_apply_eq, mul_one, add_comm]
  · simp_rw [mul_adjp_apply_ne A i j h, one_apply_ne h, mul_zero]

Похожие утверждения