of_symm_single — Mathlib

English

The symmetrized of the single matrix corresponds to the single in the opposite basis.

Русский

Обратное отображение к одинокой матрице соответствует одиночной матрице в противоположной базе.

LaTeX

$$$\mathrm{of}\,\mathrm{symm}(\text{single } i j a) = \text{Pi.single } i (\text{Pi.single } j a).$$$

Lean4

@[simp]
theorem of_symm_single (i : m) (j : n) (a : α) : of.symm (single i j a) = Pi.single i (Pi.single j a) :=
  congr_arg of.symm <| single_eq_of_single_single i j a

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