map_id' — Mathlib

English

The identity map on α, viewed through Sym2, is the identity operation: map id = id.

Русский

Идеальное отображение на α через Sym2 отождествляется с обычным отображением: map id = id.

LaTeX

$$$ \\operatorname{Sym2.map} \\mathrm{id} = \\mathrm{id}. $$$

Lean4

/-- Note: `Sym2.map_id` will not simplify `Sym2.map id z` due to `Sym2.map_congr`. -/
@[simp]
theorem map_id' : (map fun x : α => x) = id :=
  map_id

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