stabilizerIsoEnd_symm_apply — Mathlib

English

The inverse of the stabilizer-endomorphism is the identity on endomorphisms; applying the inverse to f gives f.

Русский

Обратный образ стабилизатора-эндоморфизма действует как тождественный на эндоморфизмы; применяя обратное к f, получаем f.

LaTeX

$$$(stabilizerIsoEnd\ M\ x).symm\ f = f$$$

Lean4

@[simp 1100]
theorem stabilizerIsoEnd_symm_apply (f : End _) : (stabilizerIsoEnd M x).symm f = f :=
  rfl

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