comp_symm_single — Mathlib

English

The symmetry of comp on a singleton equals the composition of the symmetry on the blocks.

Русский

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

LaTeX

$$$ \mathrm{comp}_{I J K L R}^{-1}(\mathrm{single}(ii, jj, r)) = \mathrm{single}(ii.fst, jj.fst, \mathrm{single}(ii.snd, jj.snd, r)) $$$

Lean4

@[simp]
theorem comp_symm_single [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (ii jj r) :
    (comp I J K L R).symm (single ii jj r) = (single ii.1 jj.1 (single ii.2 jj.2 r)) :=
  (comp I J K L R).symm_apply_eq.2 <| comp_single_single _ _ _ _ _ |>.symm

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