mul_adjp_apply_eq — Mathlib

English

If i ≠ j, the (i,j) entry of A · adjp(1) A equals the (i,j) entry of A · adjp(-1) A.

Русский

При i ≠ j, элементы (i,j) в произведении A · adjp(1) A и A · adjp(-1) A совпадают.

LaTeX

$$$(A \\cdot \\operatorname{adjp}(1) A)_{ij} = (A \\cdot \\operatorname{adjp}(-1) A)_{ij} \\quad (i \\neq j)$$$

Lean4

theorem mul_adjp_apply_eq : (A * adjp s A) i i = detp s A :=
  by
  have key := sum_fiberwise_eq_sum_filter (ofSign s) univ (· i) fun σ ↦ ∏ k, A k (σ k)
  simp_rw [mem_univ, filter_true] at key
  simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]
  refine sum_congr rfl fun x hx ↦ sum_congr rfl fun σ hσ ↦ ?_
  rw [← prod_mul_prod_compl ({ i } : Finset n), prod_singleton, (mem_filter.mp hσ).2]

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