English
If A,B are square with determinants units, then the sum detp 1 A · detp (-1) B + detp (-1) A · detp 1 B is AddUnit.
Русский
Пусть A,B — квадратные матрицы и их детерминанты — единицы; сумма detp 1 A · detp (-1) B + detp (-1) A · detp 1 B является AddUnit.
LaTeX
$$$\\text{IsAddUnit}(\\detp(1)A \\cdot \\detp(-1)B + \\detp(-1)A \\cdot \\detp(1)B)$$$
Lean4
theorem isAddUnit_detp_mul_detp (hAB : A * B = 1) : IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) :=
by
suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A * detp t B) from (h (by decide)).add (h (by decide))
intro s t h
simp_rw [detp, sum_mul_sum, IsAddUnit.sum_iff]
intro σ hσ τ hτ
rw [mem_ofSign] at hσ hτ
rw [← hσ, ← hτ, ← sign_inv] at h
replace h := ne_of_apply_ne sign h
rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one, eq_comm] at h
simp_rw [Equiv.ext_iff, not_forall, Perm.mul_apply, Perm.one_apply] at h
obtain ⟨k, hk⟩ := h
rw [mul_comm, ← Equiv.prod_comp σ, mul_comm, ← prod_mul_distrib, ← mul_prod_erase univ _ (mem_univ k), ← smul_eq_mul]
exact (isAddUnit_mul hAB k (τ (σ k)) (σ k) hk).smul_right _
