conj_refl — Mathlib

English

Conjugating by the identity equivalence leaves the endomorphism structure unchanged: conj(id_α) equals id_{α→α}.

Русский

Сопряжение по тождественному отображению не изменяет наборы эндоморфизмов: conj(identity) равняется identity на α→α.

LaTeX

$$$ \operatorname{conj}(\mathrm{id}_\alpha) = \mathrm{id}_{\alpha \to \alpha} $$$

Lean4

@[simp]
theorem conj_refl : conj (Equiv.refl α) = Equiv.refl (α → α) :=
  rfl

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