English
In a finite-dimensional space, if linear maps are inverse to each other on one side then they are inverse on the other side.
Русский
В конечном размерном пространстве, если линейные отображения являются взаимно обратными слева, то они взаимно обратны и справа.
LaTeX
$$$[\text{FiniteDimensional}_K V] \{f,g: V \to V\} : f g = 1 \Rightarrow g f = 1$$$
Lean4
/-- In a finite-dimensional space, if linear maps are inverse to each other on one side then they
are also inverse to each other on the other side. -/
theorem mul_eq_one_of_mul_eq_one [FiniteDimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) : g * f = 1 :=
by
have ginj : Injective g := HasLeftInverse.injective ⟨f, fun x => show (f * g) x = (1 : V →ₗ[K] V) x by rw [hfg]⟩
let ⟨i, hi⟩ := g.exists_rightInverse_of_surjective (range_eq_top.2 (injective_iff_surjective.1 ginj))
have : f * (g * i) = f * 1 := congr_arg _ hi
rw [← mul_assoc, hfg, one_mul, mul_one] at this; rwa [← this]
