ofInjectiveEndo_left_inv — Mathlib

English

The inverse on the left of the injective endomorphism f composed with f yields the identity.

Русский

Левая обратная связь для инъективного эндоморфизма f и f образуют тождество.

LaTeX

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

Lean4

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

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