English
For an R-linear endomorphism f of M, f is a unit in the endomorphism ring End_R(M) if and only if f is bijective as a function.
Русский
Для линейного эндоморфизма f на M выполняется: f является единицей в кольце эндоморфизмов End_R(M) тогда и только тогда, когда f — биекция как отображение.
LaTeX
$$$ \text{IsUnit}(f) \iff \text{Bijective}(f) $$$
Lean4
theorem _root_.Module.End.isUnit_iff [Module R M] (f : Module.End R M) : IsUnit f ↔ Function.Bijective f :=
⟨fun h ↦
Function.bijective_iff_has_inverse.mpr <|
⟨h.unit.inv, ⟨Module.End.isUnit_inv_apply_apply_of_isUnit h, Module.End.isUnit_apply_inv_apply_of_isUnit h⟩⟩,
fun H ↦
let e : M ≃ₗ[R] M := { f, Equiv.ofBijective f H with }
⟨⟨_, e.symm, LinearMap.ext e.right_inv, LinearMap.ext e.left_inv⟩, rfl⟩⟩
