coe_ofInjectiveOfFinrankEq — Mathlib

English

The left inverse of the injective endomorphism corresponds to the inverse map on the left.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coe_ofInjectiveOfFinrankEq (f : V →ₗ[K] V') (hinj : Function.Injective f)
    (hrank : Module.finrank K V = Module.finrank K V') : (ofInjectiveOfFinrankEq f hinj hrank).toLinearMap = f :=
  rfl

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