simple_mul_simple_pow' — Mathlib

English

If the matrix is symmetric, the corresponding relation can be read in the opposite order: (s_j s_i)^{M(j,i)} = 1.

Русский

Если матрица симметрична, соответствующее отношение читается в обратном порядке: (s_j s_i)^{M(j,i)} = 1.

LaTeX

$$$(s_j s_i)^{M(j,i)} = 1$$

Lean4

@[simp]
theorem simple_mul_simple_pow' (i i' : B) : (s i' * s i) ^ M i i' = 1 :=
  M.symmetric i' i ▸ cs.simple_mul_simple_pow i' i

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