ext — Mathlib

English

If two maps agree after composition with f, they are equal.

Русский

Если два отображения согласуются после композиции с f, они равны.

LaTeX

$$$$ j = k \;\Rightarrow\; j\circ f = k\circ f \text{ implies } j = k. $$$$

Lean4

theorem ext (map_unit : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) ⦃j k : M' →ₗ[R] M''⦄
    (h : j.comp f = k.comp f) : j = k :=
  by
  rw [← lift_unique S f (k.comp f) map_unit j h, lift_unique]
  rfl

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