English
For A,B with AB = I, the identity A + [detp(1)A · adjp(−1)B + detp(−1)A · adjp(1)B] = [detp(1)A · adjp(1)B + detp(−1)A · adjp(−1)B] holds.
Русский
При AB = I верно тождество A + [detp(1)A · adjp(−1)B + detp(−1)A · adjp(1)B] = [detp(1)A · adjp(1)B + detp(−1)A · adjp(−1)B].
LaTeX
$$$A + (\detp(1)A \cdot \operatorname{adj}_p(-1)B + \detp(-1)A \cdot \operatorname{adj}_p(1)B) = \detp(1)A \cdot \operatorname{adj}_p(1)B + \detp(-1)A \cdot \operatorname{adj}_p(-1)B$$$
Lean4
theorem detp_smul_adjp (hAB : A * B = 1) :
A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B :=
by
have h0 := detp_mul A B
rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0
have h := detp_smul_add_adjp hAB
replace h := congr(detp 1 A • $h + detp (-1) A • $h.symm)
simp only [smul_add, smul_smul] at h
rwa [add_add_add_comm, ← add_smul, add_add_add_comm, ← add_smul, ← h0, add_smul, one_smul, add_comm A, add_assoc,
((isAddUnit_detp_mul_detp hAB).smul_right _).add_right_inj] at h
