injective_of_comp_eq_id — Mathlib

English

If a function g is a left and right inverse of a linear map f, then g is itself linear.

Русский

Если функция g является левым и правым обратным линейного отображения f, то g сама по себе линейна.

LaTeX

$$$\text{If } g\circ f = \mathrm{id} \text{ and } f\circ g = \mathrm{id}, \text{ then } g\text{ is linear.}$$$

Lean4

theorem injective_of_comp_eq_id : Injective f :=
  .of_comp (f := g) <| by simp_rw [← coe_comp, h, id_coe, bijective_id.1]

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