pOpcycles_opcyclesToCycles — Mathlib

English

The map pOpcycles i followed by opcyclesToCycles i j equals toCycles i j map.

Русский

Образ pOpcycles i затем opcyclesToCycles i j равен toCycles i j.

LaTeX

$$$K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i j$$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_opcyclesToCycles : K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i j := by
  simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles, p_fromOpcycles, toCycles_i]

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