unsym — Mathlib

English

There is a canonical inverse equivalence from αˢʸᵐ to α, given by the identity map.

Русский

Существует каноническое обратное эквивалентное отображение от αˢʸᵐ к α, заданное как тождественное отображение.

LaTeX

$$$\text{SymAlg.unsym}: \alpha^{\text{sym}} \cong \alpha ext{ is the identity inverse}$$$

Lean4

/-- The element of `α` represented by `x : αˢʸᵐ`. -/
-- We add `@[pp_nodot]` in case RFC https://github.com/leanprover/lean4/issues/6178 happens.

@[pp_nodot]
def unsym : αˢʸᵐ ≃ α :=
  Equiv.refl _

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