homotopyHσToZero — Mathlib

English

There exists a null-homotopy showing Hσ q is homotopic to the zero map, i.e., the corresponding homotopy between Hσ q and 0 is explicit.

Русский

Существует нулевой гомотоп, показывающий, что Hσ q гомотопен к нулевому отображению; явен соответствующий гомотоп.

LaTeX

$$$$ \text{Hσ}_q \simeq 0 \;\text{ via }\; \text{homotopy} $$$$

Lean4

/-- `Hσ` is null homotopic -/
def homotopyHσToZero (q : ℕ) : Homotopy (Hσ q : K[X] ⟶ K[X]) 0 :=
  nullHomotopy' (hσ' q)

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