isAddUnit_mul — Mathlib

English

For any i ≠ j, the i,j-entry of A·adjp 1 A equals the i,j-entry of A·adjp(-1) A; a refinement of the previous diagonal/result statements.

Русский

Для любых i ≠ j, элемент (i,j) в A·adjp(1)A совпадает с элементом (i,j) в 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 isAddUnit_mul (hAB : A * B = 1) (i j k : n) (hij : i ≠ j) : IsAddUnit (A i k * B k j) :=
  by
  revert k
  rw [← IsAddUnit.sum_univ_iff, ← mul_apply, hAB, one_apply_ne hij]
  exact isAddUnit_zero

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