English
The transpose of the adjugate equals the adjugate of the transpose: (adjugate A)^T = adjugate(A^T).
Русский
Транспонирование adjugate равно adjugate транспонированной матрицы: (adjugate A)^T = adjugate(A^T).
LaTeX
$$$$ (\\operatorname{adjugate} A)^{\\top} = \\operatorname{adjugate}(A^{\\top}). $$$$
Lean4
theorem adjugate_transpose (A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ :=
by
ext i j
rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]
rw [det_apply', det_apply']
apply Finset.sum_congr rfl
intro σ _
congr 1
by_cases h : i = σ j
· -- Everything except `(i, j)` (= `(σ j, j)`) is given by A, and the rest is a single `1`.
congr
ext j'
subst h
have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
rw [updateRow_apply, updateCol_apply]
simp_rw [this]
rw [← dite_eq_ite, ← dite_eq_ite]
congr 1 with rfl
rw [Pi.single_eq_same, Pi.single_eq_same]
· -- Otherwise, we need to show that there is a `0` somewhere in the product.
have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 :=
by
apply prod_eq_zero (mem_univ j)
rw [updateCol_self, Pi.single_eq_of_ne' h]
rw [this]
apply prod_eq_zero (mem_univ (σ⁻¹ i))
erw [apply_symm_apply σ i, updateRow_self]
apply Pi.single_eq_of_ne
intro h'
exact h ((symm_apply_eq σ).mp h')
