permCongr_refl — Mathlib

English

Conjugating by e sends the identity permutation to the identity permutation: e.permCongr (Equiv.refl _) = Equiv.refl _.

Русский

Конъюгация перестановок по e отображает тождественную перестановку в тождественную перестановку: e.permCongr (refl) = refl.

LaTeX

$$$e\text{.permCongr}(\mathrm{id}) = \mathrm{id}$$$

Lean4

@[simp]
theorem permCongr_refl : e.permCongr (Equiv.refl _) = Equiv.refl _ := by simp [permCongr_def]

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