one_def

Mathlib.Topology.Homotopy.HomotopyGroup

URI: https://scilib.ai/kg/mathlib#HomotopyGroup.one_def

English

The multiplicative identity in a nonempty index set corresponds to the constant GenLoop.

Русский

Единица умножения для непустого индекса равна константной петле GenLoop.

LaTeX

$$$1 = \\llbracket \\mathrm{const}\\rrbracket$ in HomotopyGroup$$

Lean4

/-- Characterization of multiplicative identity -/
theorem one_def [Nonempty N] : (1 : HomotopyGroup N X x) = ⟦const⟧ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru