English
The determinant of a product equals the product of determinants: det(MN) = det(M) det(N).
Русский
Детерминант произведения равен произведению детерминантов: det(MN) = det(M) det(N).
LaTeX
$$$\\det(MN) = \\det(M) \\det(N)$$$
Lean4
theorem det_mul_aux {M N : Matrix n n R} {p : n → n} (H : ¬Bijective p) :
(∑ σ : Perm n, ε σ * ∏ x, M (σ x) (p x) * N (p x) x) = 0 :=
by
obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j :=
by
rw [← Finite.injective_iff_bijective, Injective] at H
push_neg at H
exact H
exact
sum_involution (fun σ _ => σ * Equiv.swap i j)
(fun σ _ =>
by
have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])
simp [this, sign_swap hij, -sign_swap', prod_mul_distrib])
(fun σ _ _ => (not_congr mul_swap_eq_iff).mpr hij) (fun _ _ => mem_univ _) fun σ _ => mul_swap_involutive i j σ
