one_trans — Mathlib

English

The identity permutation acts as a left identity for trans of any permutation: (1 : Perm α).trans e = e.

Русский

Тождественная перестановка слева выступает как единичный элемент для преобразования trans: (1 : Perm α).trans e = e.

LaTeX

$$$\\\\forall {\\alpha} {e : \\\\mathrm{Perm} \\\\alpha}, \\\\; (1 : \\\\mathrm{Perm} \\\\alpha).trans e = e$$$

Lean4

@[simp]
theorem one_trans {α : Type*} {β : Sort*} (e : α ≃ β) : (1 : Perm α).trans e = e :=
  rfl

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