mul_spec — Mathlib

English

The inverse in the homotopy group is given by reversing along any coordinate i.

Русский

Обратное в гомотопической группе задаётся разворотом вдоль любой координаты i.

LaTeX

$$$ (\\llbracket p \\rrbracket)^{-1} = \\llbracket \\mathrm{symmAt}\\ i\\ p \\rrbracket $$$

Lean4

/-- Characterization of multiplication -/
theorem mul_spec [Nonempty N] {i} {p q : Ω^ N X x} :
    -- TODO: introduce `HomotopyGroup.mk` and remove defeq abuse.
    ((· * ·) : _ → _ → HomotopyGroup N X x) ⟦p⟧ ⟦q⟧ = ⟦transAt i q p⟧ :=
  by
  rw [transAt_indep (Classical.arbitrary N) q, ← fromLoop_trans_toLoop]
  apply Quotient.sound
  rfl

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