fromOpcycles_naturality — Mathlib

English

The naturality with respect to fromOpcycles: opcyclesMap φ ≫ S₂.fromOpcycles = S₁.fromOpcycles ≫ φ.τ₃.

Русский

Натурализм по fromOpcycles: opcyclesMap φ ∘ S₂.fromOpcycles = S₁.fromOpcycles ∘ φ.τ₃.

LaTeX

$$$opcyclesMap\phi \circ S_2.fromOpcycles = S_1.fromOpcycles \circ \phi.\tau_3$$$

Lean4

@[reassoc (attr := simp)]
theorem fromOpcycles_naturality : opcyclesMap φ ≫ S₂.fromOpcycles = S₁.fromOpcycles ≫ φ.τ₃ :=
  opcyclesMap'_g' _ _ _

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