comp_id

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.comp_id

English

If g ∘ f equals the identity on M, then g is a left inverse of f, i.e., g ∘ f = id implies g is left-inverse to f as functions.

Русский

Если g ∘ f = id, то g является левым обратным к f как функциям.

LaTeX

$$$\\text{If } g\\circ f = \\mathrm{id}, \\text{ then } g = f^{-1} \\text{ on the image of } f$.$$

Lean4

@[simp]
theorem comp_id (f : M₁ →SL[σ₁₂] M₂) : f.comp (.id R₁ M₁) = f :=
  ext fun _x => rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru