mul_eq_one_comm — Mathlib

English

In a finite-dimensional space, linear maps are inverse to each other on one side iff they are inverse on the other side.

Русский

В конечномерном пространстве линейные отображения взаимно обратны слева тогда и только тогда взаимно обратны справа.

LaTeX

$$$[\operatorname{FiniteDimensional}_K V] {f,g: V \to V} : (f g = 1) \iff (g f = 1)$$$

Lean4

/-- In a finite-dimensional space, linear maps are inverse to each other on one side if and only if
they are inverse to each other on the other side. -/
theorem mul_eq_one_comm [FiniteDimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1 :=
  ⟨mul_eq_one_of_mul_eq_one, mul_eq_one_of_mul_eq_one⟩

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