p_opcyclesMap — Mathlib

English

The pOpcycles and opcyclesMap commute with φ: S₁.pOpcycles ≫ opcyclesMap φ = φ.τ₂ ≫ S₂.pOpcycles.

Русский

Согласование pOpcycles и opcyclesMap через φ: S₁.pOpcycles ≫ opcyclesMap φ = φ.τ₂ ≫ S₂.pOpcycles.

LaTeX

$$$S_1.pOpcycles \circ opcyclesMap \phi = \phi.\tau_2 \circ S_2.pOpcycles$$$

Lean4

@[reassoc (attr := simp)]
theorem p_opcyclesMap : S₁.pOpcycles ≫ opcyclesMap φ = φ.τ₂ ≫ S₂.pOpcycles :=
  p_opcyclesMap' _ _ _

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