comp_eq_id_comm — Mathlib

English

On a finite-dimensional space, f composed with g equals the identity if and only if g composed with f equals the identity.

Русский

На конечномерном пространстве композиция f ∘ g равна идентичности тогда и только тогда, когда g ∘ f равна идентичности.

LaTeX

$$$[\operatorname{FiniteDimensional}_K V] \{f,g: V \to V\} : f \circ g = \mathrm{Id} \iff g \circ f = \mathrm{Id}$$$

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 comp_eq_id_comm [FiniteDimensional K V] {f g : V →ₗ[K] V} : f.comp g = id ↔ g.comp f = id :=
  mul_eq_one_comm

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