cyclesMap_i — Mathlib

English

The cyclesMap between S1 and S2 is compatible with the i-cycles inclusions: cyclesMap φ followed by S2.iCycles equals S1.iCycles followed by φ.τ₂.

Русский

Циклы Map между S1 и S2 совместимы с включениями i циклов: cyclesMap φ затем S2.iCycles равно S1.iCycles затем φ.τ₂.

LaTeX

$$$cyclesMap(\phi) \circ S_2.iCycles = S_1.iCycles \circ \phi.\tau_2$$$

Lean4

@[reassoc (attr := simp)]
theorem cyclesMap_i : cyclesMap φ ≫ S₂.iCycles = S₁.iCycles ≫ φ.τ₂ :=
  cyclesMap'_i _ _ _

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