detp_smul_add_adjp — Mathlib

English

If A and B are square matrices with AB = I, then detp(1)B · A + adjp(−1)B equals detp(−1)B · A + adjp(1)B.

Русский

Если A и B — квадратные матрицы и AB = I, тогда detp(1)B · A + adjp(−1)B равно detp(−1)B · A + adjp(1)B.

LaTeX

$$$\text{If } AB=I, \; \ detp(1)B \cdot A + \operatorname{adj}_p(-1)B = \ detp(-1)B \cdot A + \operatorname{adj}_p(1)B.$$$

Lean4

theorem detp_smul_add_adjp (hAB : A * B = 1) : detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B :=
  by
  have key := congr(A * $(mul_adjp_add_detp B))
  simp_rw [mul_add, ← mul_assoc, hAB, one_mul, mul_smul, mul_one] at key
  rwa [add_comm, eq_comm, add_comm]

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