cancel_right

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.cancel_right

English

If f is injective, then f ∘ g is injective as a function of g, i.e., f injective implies g ↦ f ∘ g is injective.

Русский

Если f инъективно, тогда f ∘ g инъективно как функция по g.

LaTeX

$$$\text{If } f \text{ is injective, then } (g \mapsto f \circ g) \text{ is injective}. $$$

Lean4

@[simp]
theorem cancel_right (hg : Surjective g) : f.comp g = f'.comp g ↔ f = f' :=
  hg.injective_linearMapComp_right.eq_iff

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

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

Разделы

Аффилиация

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