ofInjectiveEndo_right_inv — Mathlib

English

For an injective endomorphism f, the composition with its inverse on the right yields the identity.

Русский

Для инъективного эндоморфизма f композиция f с его обратной по правой стороне дает тождество.

LaTeX

$$$f \circ (\operatorname{ofInjectiveEndo} f h\_inj)^{-1} = \mathrm{Id}$$$

Lean4

@[simp]
theorem ofInjectiveEndo_right_inv (f : V →ₗ[K] V) (h_inj : Injective f) : f * (ofInjectiveEndo f h_inj).symm = 1 :=
  LinearMap.ext <| (ofInjectiveEndo f h_inj).apply_symm_apply

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