inv_trans_self — Mathlib

English

For any e ∈ Perm α, e^{-1} trans e = 1; i.e. e^{-1} then e equals the identity.

Русский

Для любого e ∈ Perm α, e^{-1} trans e = 1; то есть сначала применяется обратная перестановка, затем сама перестановка, дают тождество.

LaTeX

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

Lean4

@[simp]
theorem inv_trans_self (e : Perm α) : e⁻¹.trans e = 1 :=
  Equiv.symm_trans_self e

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