T_S_rel_smul — Mathlib

English

A composite action identity holds: S^3 T S T S acts as T^{-1} on any FixedDetMatrix.

Русский

Составное действие удовлетворяет тождеству: S^3 T S T S действует как T^{-1} на FixedDetMatrix.

LaTeX

$$$S^3 T S T S \cdot A = T^{-1} \cdot A$ for A in FixedDetMatrix.$$

Lean4

@[simp]
theorem T_S_rel_smul (A : Δ m) : S • S • S • T • S • T • S • A = T⁻¹ • A := by simp_rw [← T_S_rel, ← smul_assoc]

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