isUnit_inv_apply_apply_of_isUnit

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.isUnit_inv_apply_apply_of_isUnit

English

If f is a unit in End_R(M), then applying the inverse of f to f(x) gives x; equivalently f^{-1}(f(x)) = x for all x ∈ M.

Русский

Пусть f является обратимым в End_R(M); тогда f^{-1}(f(x)) = x для всех x ∈ M.

LaTeX

$$$\\forall x\\in M,\\; f^{-1}(f(x))=x.$$$

Lean4

theorem isUnit_inv_apply_apply_of_isUnit {f : End R M} (h : IsUnit f) (x : M) : h.unit.inv (f x) = x :=
  (by simp : (h.unit.inv * f) x = x)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru