freeGroupEmptyEquivUnit — Mathlib

English

The bijection between FreeGroup Empty and Unit is defined by sending the empty word to the unit and vice versa.

Русский

Биекция между FreeGroup Empty и Unit задаётся как отображение пустого слова в единицу и обратно.

LaTeX

$$$ freeGroupEmptyEquivUnit : FreeGroup Empty \\simeq Unit $$$

Lean4

/-- The bijection between the free group on the empty type, and a type with one element. -/
@[to_additive /-- The bijection between the additive free group on the empty type, and a type with
      one element. -/
    ]
def freeGroupEmptyEquivUnit : FreeGroup Empty ≃ Unit
    where
  toFun _ := ()
  invFun _ := 1
  left_inv := by rintro ⟨_ | ⟨⟨⟨⟩, _⟩, _⟩⟩; rfl

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